Merge pull request #219 from Deducteam/acu-merge

Merge of #189 and #203

api/env.ml

@@ -15,6 +15,7 @@ let set_debug_mode =
       | 'c' -> Debug.enable_flag  Confluence.d_confluence
       | 'u' -> Debug.enable_flag  Typing.d_rule
       | 't' -> Debug.enable_flag  Typing.d_typeChecking
+      | 's' -> Debug.enable_flag  Srcheck.d_SR
       | 'r' -> Debug.enable_flag  Reduction.d_reduce
       | 'm' -> Debug.enable_flag  Matching.d_matching
       | c -> raise (DebugFlagNotRecognized c)
@@ -65,7 +66,7 @@ sig
   val define      : loc -> ident -> Signature.scope ->
                     bool -> term -> term option -> unit
   val add_rules   : Rule.partially_typed_rule list ->
-                    (Subst.Subst.t * Rule.typed_rule) list
+                    (Exsubst.ExSubst.t * Rule.typed_rule) list
 
   val infer            : ?ctx:typed_context -> term         -> term
   val check            : ?ctx:typed_context -> term -> term -> unit
@@ -124,9 +125,16 @@ struct
     with e -> raise_as_env lc e
 
   let _declare lc (id:ident) scope st ty : unit =
-    match T.inference !sg ty with
-    | Kind | Type _ -> Signature.add_declaration !sg lc id scope st ty
-    | s -> raise (Typing.Typing_error (Typing.SortExpected (ty,[],s)))
+    Signature.add_declaration !sg lc id scope st
+      ( match T.inference !sg ty, st with
+        | Kind  , Definable AC
+        | Kind  , Definable (ACU _)   ->
+           raise (Typing_error (SortExpected (ty,[],mk_Kind) ))
+        | Type _, Definable AC        -> mk_Arrow dloc ty (mk_Arrow dloc ty ty)
+        | Type _, Definable (ACU neu) -> ignore(T.checking !sg neu ty);
+          mk_Arrow dloc ty (mk_Arrow dloc ty ty)
+        | Kind, _ | Type _, _ -> ty
+        | s, _ -> raise (Typing_error (SortExpected (ty,[],s)))  )
 
   let is_injective lc cst = Signature.is_injective !sg lc cst
 
@@ -154,9 +162,8 @@ struct
 
   (** Checks that all rule are left-linear. *)
   let _check_ll (r:rule_infos) : unit =
-    List.iter
-      (function Linearity _ -> raise (Env_error (Some (get_name()), r.l, NonLinearRule r.name)) | _ -> ())
-      r.constraints
+    if r.nonlinear <> []
+    then raise (Env_error (Some (get_name()), r.l, NonLinearRule r.name))
 
   let _add_rules rs =
     let ris = List.map Rule.to_rule_infos rs in
@@ -174,7 +181,7 @@ struct
     | _ ->
       if opaque then Signature.add_declaration !sg lc id scope Signature.Static ty
       else
-        let _ = Signature.add_declaration !sg lc id scope Signature.Definable ty in
+        let _ = Signature.add_declaration !sg lc id scope (Signature.Definable Free) ty in
         let cst = mk_name (get_name ()) id in
         let rule =
           { name= Delta(cst) ;
@@ -193,7 +200,7 @@ struct
     try _define lc id scope op te ty_opt
     with e -> raise_as_env lc e
 
-  let add_rules (rules: partially_typed_rule list) : (Subst.Subst.t * typed_rule) list =
+  let add_rules (rules: partially_typed_rule list) : (Exsubst.ExSubst.t * typed_rule) list =
     try
       let rs2 = List.map (T.check_rule !sg) rules in
       _add_rules rules;

api/env.mli

@@ -88,7 +88,7 @@ sig
   val define      : loc -> ident -> Signature.scope -> bool -> term -> term option -> unit
   (** [define l id scope body ty] defines the symbol [id] of type [ty] to be an alias of [body]. *)
 
-  val add_rules   : Rule.partially_typed_rule list -> (Subst.Subst.t * Rule.typed_rule) list
+  val add_rules   : Rule.partially_typed_rule list -> (Exsubst.ExSubst.t * Rule.typed_rule) list
   (** [add_rules rule_lst] adds a list of rule to a symbol. All rules must be on the
       same symbol. *)
 

api/errors.ml

@@ -155,6 +155,10 @@ let fail_dtree_error file md errid err =
     fail lc
       "The definable symbol '%a' inside the rewrite rules for \ '%a' should have the same arity when they are on the same column."
       pp_ident id pp_ident rid
+  | ACSymbolRewritten (lc, cst, _) ->
+    fail lc
+      "Rewrite rules for AC definable symbol '%a' should not have arity 0."
+      pp_name cst
 
 let fail_rule_error file md errid err =
   let fail lc = fail_exit 3 errid file md (Some lc) in
@@ -204,6 +208,8 @@ let fail_signature_error file md errid def_loc err =
     fail lc "Fail to open module '%s'." md
   | SymbolNotFound (lc,cst) ->
     fail lc "Cannot find symbol '%a'." pp_name cst
+  | ExpectedACUSymbol (lc,cst) ->
+    fail lc "Expected ACU symbol '%a'." pp_name cst
   | AlreadyDefinedSymbol (lc,n) ->
     fail lc "Already declared symbol '%a'." pp_name n
   | CannotBuildDtree err -> fail_dtree_error file md errid err
@@ -285,6 +291,7 @@ let code : exn -> int =
             begin match e with
               | Dtree.HeadSymbolMismatch _                   -> 300
               | Dtree.ArityInnerMismatch _                   -> 301
+              | Dtree.ACSymbolRewritten _                    -> 310
             end
           | Signature.CannotMakeRuleInfos _                  -> 302
           | Signature.UnmarshalBadVersionNumber _            -> 303
@@ -298,6 +305,7 @@ let code : exn -> int =
           | Signature.GuardNotSatisfied _                    -> 401
           | Signature.CouldNotExportModule _                 -> 402
           | Signature.PrivateSymbol _                        -> 403
+          | Signature.ExpectedACUSymbol _                    -> 404
         end
       | EnvErrorRule e ->
         begin

api/pp.ml

@@ -245,32 +245,35 @@ let print_red_cfg fmt cfg =
 
 let print_entry fmt e =
   let open Format in
+  let scope_to_string = function
+    | Signature.Public  -> ""
+    | Signature.Private -> "private "
+  in
   match e with
-  | Decl(_,id,Public,Signature.Static,ty) ->
-    fprintf fmt "@[<2>%a :@ %a.@]@.@." print_ident id print_term ty
-  | Decl(_,id,Private,Signature.Static,ty) ->
-    fprintf fmt "@[<2>private %a :@ %a.@]@.@." print_ident id print_term ty
-  | Decl(_,id,Public,Signature.Definable,ty) ->
-    fprintf fmt "@[<2>def %a :@ %a.@]@.@." print_ident id print_term ty
-  | Decl(_,id,Private,Signature.Definable,ty) ->
-     fprintf fmt "@[<2>private def %a :@ %a.@]@.@." print_ident id print_term ty
-  | Decl(_,id,Public,Signature.Injective,ty) ->
-    fprintf fmt "@[<2>injective %a :@ %a.@]@.@." print_ident id print_term ty
-  | Decl(_,id,Private,Signature.Injective,ty) ->
-    fprintf fmt "@[<2>private injective %a :@ %a.@]@.@." print_ident id print_term ty
-  | Def(_,id,scope,opaque,ty,te)  ->
-     let key =
-       match scope, opaque with
-       | Public , true  -> "thm"
-       | Public , false -> "def"
-       | Private, true  -> "private thm"
-       | Private, false -> "private def"
-     in
-     begin
-       match ty with
-       | None    -> fprintf fmt "@[<hv2>%s %a@ :=@ %a.@]@.@." key
+  | Decl(_,id,scope,Static,ty) ->
+     fprintf fmt "@[<2>%s%a :@ %a.@]@.@." (scope_to_string scope)
+       print_ident id print_term ty
+  | Decl(_,id,scope,Definable Free,ty) ->
+     fprintf fmt "@[<2>%sdef %a :@ %a.@]@.@." (scope_to_string scope)
+       print_ident id print_term ty
+  | Decl(_,id,scope,Injective,ty) ->
+     fprintf fmt "@[<2>%sinjective %a :@ %a.@]@.@." (scope_to_string scope)
+       print_ident id print_term ty
+  | Decl(_,id,scope,Definable AC,ty) ->
+     fprintf fmt "@[<2>%sdefac %a [@ %a].@]@.@."(scope_to_string scope)
+       print_ident id print_term ty
+  | Decl(_,id,scope,Definable ACU(neu),ty) ->
+     fprintf fmt "@[<2>%sdefacu %a [@ %a, %a].@]@.@."(scope_to_string scope)
+       print_ident id print_term ty print_term neu
+  | Def(_,id,scope,opaque,ty,te) ->
+    let key = if opaque then "thm" else "def" in
+    begin
+      match ty with
+      | None    -> fprintf fmt "@[<hv2>%s%s %a@ :=@ %a.@]@.@."
+                     (scope_to_string scope) key
                      print_ident id print_term te
-       | Some ty -> fprintf fmt "@[<hv2>%s %a :@ %a@ :=@ %a.@]@.@." key
+      | Some ty -> fprintf fmt "@[<hv2>%s%s %a :@ %a@ :=@ %a.@]@.@."
+                     (scope_to_string scope) key
                      print_ident id print_term ty print_term te
     end
   | Rules(_,rs)             ->

api/processor.ml

@@ -34,7 +34,7 @@ struct
       let rs = E.add_rules rs in
       List.iter (fun (s,r) ->
           Debug.debug Debug.d_notice "%[email protected] the following constraints: %a"
-            pp_typed_rule r (Subst.Subst.pp (fun n -> let _,n,_ = List.nth r.ctx n in n)) s) rs
+            pp_typed_rule r (Exsubst.ExSubst.pp (fun n -> let _,n,_ = List.nth r.ctx n in n)) s) rs
     | Eval(_,red,te) ->
       let te = E.reduction ~red te in
       Format.printf "%a@." Printer.print_term te
@@ -84,7 +84,7 @@ struct
       Signature.add_external_declaration sg lc (Basic.mk_name md id) scope st ty
     | Def(lc,id,scope,_,Some ty,te) ->
       let open Rule in
-      Signature.add_external_declaration sg lc (Basic.mk_name md id) scope Signature.Definable ty;
+      Signature.add_external_declaration sg lc (Basic.mk_name md id) scope (Signature.Definable Term.Free) ty;
       let cst = Basic.mk_name md id in
       let rule = { name= Delta(cst) ; ctx = [] ; pat = Pattern(lc, cst, []); rhs = te ; } in
       Signature.add_rules sg [Rule.to_rule_infos rule]

commands/dkcheck.ml

@@ -60,7 +60,8 @@ let _ =
       c : (confluence) notifies about information provided to the confluence
                      checker (when option --confluence used)
       u : (rule)     provides information about type checking of rules
-      t : (typing)   provides information about type-checking of terms
+      t : (typing)   provides information about type checking of terms
+      s : (SR)       provides information about subject reduction checking of terms
       r : (reduce)   provides information about reduction performed in terms
       m : (matching) provides information about pattern matching" )
     ; ( "-v"
@@ -92,6 +93,11 @@ let _ =
     ; ( "--type-lhs"
       , Arg.Set Typing.fail_on_unsatisfiable_constraints
       , " Forbids rules with untypable left-hand side" )
+    ; ( "--sr-check"
+      , Arg.Int (fun i -> Srcheck.srfuel := i)
+      , "LVL Sets the level of subject reduction checking to LVL.
+                   Default value is 1. Values < 0 may not terminate on
+                   rules that do not preserve typing. " )
     ; ( "--snf"
       , Arg.Set Errors.errors_in_snf
       , " Normalizes all terms printed in error messages" )

kernel/ac.ml

@@ -0,0 +1,61 @@
+open Basic
+open Term
+
+(*   AC identifier (name and algebra).   *)
+
+type ac_ident = name * algebra
+
+let ac_ident_eq (name,_) (name',_) = name_eq name name'
+
+let pp_ac_ident fmt (name,_) = Format.fprintf fmt "%a" pp_name name
+
+(* AC functions *)
+
+let get_AC_args name = function
+  | App( Const (_,name'), a1, [a2]) when name_eq name name' -> Some (a1, a2)
+  | _ -> None
+
+(* Reduces subterms with f to have a maximal set of elements. *)
+let force_flatten_AC_terms
+      (snf:term -> term)
+      (are_convertible:term -> term -> bool)
+      (name,aci) terms =
+  let rec aux acc = function
+  | [] -> acc
+  | hd :: tl ->
+     match get_AC_args name hd with
+     | Some (a1,a2) -> aux acc (a1 :: a2 :: tl)
+     | None         ->
+        let snfhd = snf hd in
+        match get_AC_args name snfhd with
+        | Some (a1,a2) -> aux acc (a1 :: a2 :: tl)
+        | None         -> aux (snfhd :: acc) tl in
+  let res = aux [] terms in
+  (* If aci is an ACU symbol, remove corresponding neutral element. *)
+  match aci with
+  | ACU neu -> List.filter (fun x -> not (are_convertible neu x)) res
+  | _ -> res
+
+
+(* Reduces subterms with f to have a maximal set of elements. *)
+let force_flatten_AC_term
+      (snf:term -> term)
+      (are_convertible:term -> term -> bool)
+      aci t = force_flatten_AC_terms snf are_convertible aci [t]
+
+let flatten_AC_terms name =
+  let rec aux acc = function
+  | [] -> acc
+  | hd :: tl ->
+     match get_AC_args name hd with
+     | Some (a1,a2) -> aux acc (a1 :: a2 :: tl)
+     | None         -> aux (hd :: acc) tl in
+  aux []
+
+let flatten_AC_term name t = flatten_AC_terms name [t]
+
+let rec unflatten_AC (name,alg) = function
+  | [] -> ( match alg with ACU neu -> neu | _ -> assert false )
+  | [t] -> t
+  | t1 :: t2 :: tl ->
+     unflatten_AC (name,alg) ((mk_App (mk_Const dloc name) t1 [t2]) :: tl)

kernel/ac.mli

@@ -0,0 +1,27 @@
+open Basic
+open Term
+
+type ac_ident = name * algebra
+
+val ac_ident_eq : ac_ident -> ac_ident -> bool
+
+val pp_ac_ident : ac_ident printer
+
+val force_flatten_AC_term :
+  (term -> term) ->
+  (term -> term -> bool) ->
+  ac_ident -> term -> term list
+(** [force_flatten_AC_term snf are_convertible aci t]
+    returns the list [t1 ; ... ; tn] where
+    [t] is convertible with  [t1 + ... + tn] and
+    [aci] represents the AC(U) operator [+] while
+    [whnf] is used to reduce to head normal form to check for [+] symbol
+    at the head. All [ti] are reduced with [whnf].
+    [are_convertible] checks convertibility to neutral element if needed.
+ *)
+
+val flatten_AC_terms : name -> term list -> term list
+
+val flatten_AC_term  : name -> term -> term list
+
+val unflatten_AC : ac_ident -> term list -> term

kernel/basic.ml

@@ -56,7 +56,8 @@ module LList = struct
   let is_empty x = x.len = 0
   let of_list  lst = {len=List.length lst ; lst}
   let of_array arr = {len=Array.length arr; lst=Array.to_list arr}
-  let map f {len;lst} = {len; lst=List.map f lst}
+  let map  f {len;lst} = {len; lst=List.map  f lst}
+  let mapi f {len;lst} = {len; lst=List.mapi f lst}
   let nth l i = assert (i<l.len); List.nth l.lst i
 end
 

kernel/basic.mli

@@ -61,6 +61,7 @@ module LList : sig
   val of_list  : 'a list  -> 'a t
   val of_array : 'a array -> 'a t
   val map : ('a -> 'b) -> 'a t -> 'b t
+  val mapi : (int -> 'a -> 'b) -> 'a t -> 'b t
   val nth : 'a t -> int -> 'a
 end