]> matita.cs.unibo.it Git - helm.git/commitdiff
BIG FAT COMMIT REGARDING COERCIONS:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Sep 2006 15:51:36 +0000 (15:51 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Sep 2006 15:51:36 +0000 (15:51 +0000)
- multiple coercions from the same type
- coercions to funclass
- fixed cicPp for letin and pi
- improved coercions ma with a minimal test for funclass
- cheanged XML and Ast to support `Coercion ARITY label
- added syntax:
  coercion URI ARITY
  recordfield :ARITY> type
- added topological sorting module (funcotr) in extlib
- abstracted graphviz to allow non strict and tred graphs
- tentative (not yet properly done) of hiding coercions in content
- fixed a problem in metadata contraints iof there are no constraints
- renamed/moved/commented some functions (eat_prod related) in the refiner
- crossed fingers

47 files changed:
components/acic_content/cicNotationPp.ml
components/acic_content/cicNotationPt.ml
components/acic_content/cicNotationUtil.ml
components/acic_content/termAcicContent.ml
components/cic/cic.ml
components/cic/cicParser.ml
components/cic/cicUtil.ml
components/cic/cicUtil.mli
components/cic_acic/cic2Xml.ml
components/cic_acic/cic2acic.ml
components/cic_disambiguation/disambiguate.ml
components/cic_proof_checking/cicPp.ml
components/cic_unification/cicRefine.ml
components/cic_unification/cicUnification.ml
components/extlib/.depend
components/extlib/Makefile
components/extlib/graphvizPp.ml
components/extlib/graphvizPp.mli
components/extlib/hExtlib.ml
components/extlib/hExtlib.mli
components/extlib/hTopoSort.ml [new file with mode: 0644]
components/extlib/hTopoSort.mli [new file with mode: 0644]
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite/grafiteMarshal.ml
components/grafite_engine/grafiteEngine.ml
components/grafite_engine/grafiteSync.ml
components/grafite_engine/grafiteSync.mli
components/grafite_parser/grafiteParser.ml
components/lexicon/lexiconAst.ml
components/library/cicCoercion.ml
components/library/coercDb.ml
components/library/coercDb.mli
components/library/coercGraph.ml
components/library/coercGraph.mli
components/library/librarySync.ml
components/library/librarySync.mli
components/metadata/metadataConstraints.ml
components/metadata/metadataDeps.ml
components/tactics/primitiveTactics.ml
components/tactics/tactics.mli
matita/lablGraphviz.ml
matita/lablGraphviz.mli
matita/library/legacy/coq.ma
matita/library/logic/equality.ma
matita/matitaMathView.ml
matita/tests/coercions.ma

index cdc0946e6f96bd2d992984bd1043ffc3a7aa9932..49cefaec7db3f7f76652d9e24e9543bd4de9f495 100644 (file)
@@ -289,8 +289,11 @@ let pp_fields fields =
   (if fields <> [] then "\n" else "") ^ 
   String.concat ";\n" 
     (List.map 
-      (fun (name,ty,coercion) -> 
-        " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields)
+      (fun (name,ty,coercion,arity) -> 
+        " " ^ name ^ 
+        if coercion then (":" ^ 
+          if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
+        pp_term ty) fields)
         
 let pp_obj = function
  | Ast.Inductive (params, types) ->
index 609fb9d2f24a08f362c2276afa16f8fa2f673737..6ea1ec9175449da004407a76ce43f6265cbf1be9 100644 (file)
@@ -174,7 +174,7 @@ type obj =
        *   will be given in proof editing mode using the tactical language,
        *   unless the flavour is an Axiom
        *)
-  | Record of (string * term) list * string * term * (string * term * bool) list
+  | Record of (string * term) list * string * term * (string * term * bool * int) list
       (** left parameters, name, type, fields *)
 
 (** {2 Standard precedences} *)
index 8e487ed11ed293374f4737a39bbc0e975b0165ff..d9114b1808b1b5cca3da1736977718953b8adc57 100644 (file)
@@ -366,7 +366,7 @@ let freshen_obj obj =
   let index = ref 0 in
   let freshen_term = freshen_term ~index in
   let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
-  let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in
+  let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
   match obj with
   | CicNotationPt.Inductive (params, indtypes) ->
       let indtypes =
index 7948f2654ac51aa29cc79d13f12bbb3dd6a71534..516d5f5429ab56926e92e426ca654a45511b2ee5 100644 (file)
@@ -121,16 +121,31 @@ let ast_of_acic0 term_info acic k =
     | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
-       if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
-          !Acic2content.hide_coercions
+       let last_n n l =
+         let rec aux =
+          function
+             [] -> assert false
+           | [_] as l -> l,1
+           | he::tl ->
+              let (res,len) as res' = aux tl in
+               if len < n then
+                he::res,len + 1
+               else
+                res'
+         in
+          match fst (aux l) with
+             [] -> assert false
+           | [t] -> t
+           | Ast.AttributedTerm (_,(Ast.Appl l))::tl -> 
+               idref aid (Ast.Appl (l@tl))
+           | l -> idref aid (Ast.Appl l)
+       in
+       let deannot_he = Deannotate.deannotate_term he in
+       if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions
        then
-        let rec last =
-         function
-            [] -> assert false
-          | [t] -> t
-          | _::tl -> last tl
-        in
-         idref aid (k (last tl))
+         match CoercGraph.is_a_coercion_to_funclass deannot_he with
+         | None -> idref aid (last_n 1 (List.map k tl))
+         | Some i -> idref aid (last_n (i+1) (List.map k tl))
        else
         idref aid (Ast.Appl (List.map k args))
     | Cic.AAppl (aid,args) ->
index 20a6cb457dec63c700283ac952204357c38ab0de..5495872151bda13625042b884b9c8d77dd0943b3 100644 (file)
@@ -66,12 +66,13 @@ type object_flavour =
   ]
 
 type object_class =
-  [ `Coercion
+  [ `Coercion of int
   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
                       * not relevant *)
-  | `Record of (string * bool) list (** 
+  | `Record of (string * bool * int) list (** 
                         inductive type that encodes a record; the arguments are
-                        the record fields names and if they are coercions *)
+                        the record fields names and if they are coercions and
+                        then the coercion arity *)
   | `Projection     (** record projection *)
   ]
 
index 1e9a3a33c1444a553f9b7beaa8b5bee709a58254..150fe4ad983f6dab3bad1d117877e6093531b755 100644 (file)
@@ -678,7 +678,13 @@ let end_element ctxt tag =
       let class_modifiers = pop_class_modifiers ctxt in
       push ctxt
         (match pop_tag_attrs ctxt with
-        | ["value", "coercion"] -> Obj_class `Coercion
+        | ["value", "coercion"] -> Obj_class (`Coercion 0)
+        | ("value", "coercion")::["arity",n]  
+        | ("arity",n)::["value", "coercion"] -> 
+            let arity = try int_of_string n with Failure _ ->
+              parse_error "\"arity\" must be an integer"
+            in
+            Obj_class (`Coercion arity)
         | ["value", "elim"] ->
             (match class_modifiers with
             | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
@@ -691,8 +697,15 @@ let end_element ctxt tag =
                 (function
                   | Obj_field name -> 
                       (match Str.split (Str.regexp " ") name with
-                      | [name] -> name, false
-                      | [name;"coercion"] -> name,true
+                      | [name] -> name, false, 0
+                      | [name;"coercion"] -> name,true,0
+                      | [name;"coercion"; n] -> 
+                          let n = 
+                            try int_of_string n 
+                            with Failure _ -> 
+                              parse_error "int expected after \"coercion\""
+                          in
+                          name,true,n
                       | _ -> 
                           parse_error
                             "wrong \"field\"'s name attribute")
index de796910a5c7432a410470a3579a094234d6e782..6e07a4995d8ed5d436f43138a1374123b6f79f65 100644 (file)
@@ -207,6 +207,17 @@ let attributes_of_obj = function
   | Cic.CurrentProof (_, _, _, _, _, attributes)
   | Cic.InductiveDefinition (_, _, _, attributes) ->
       attributes
+
+let arity_of_composed_coercion obj =
+  let attrs = attributes_of_obj obj in
+  try
+    let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in
+    match tag with
+    |  `Class (`Coercion n) -> n
+    | _-> assert false 
+  with Not_found -> 0
+;;
+      
 let rec mk_rels howmany from =
   match howmany with 
   | 0 -> []
index b8d71f51f96da76779f64a2efc25ba58e1565750..422bb130b47a0f83b22659f49318c8e6e187c091 100644 (file)
@@ -53,6 +53,7 @@ val id_of_annterm: Cic.annterm -> Cic.id
 
 val params_of_obj: Cic.obj -> UriManager.uri list
 val attributes_of_obj: Cic.obj -> Cic.attribute list
+val arity_of_composed_coercion: Cic.obj -> int
 
 (** mk_rels [howmany] [from] 
  * creates a list of [howmany] rels starting from [from] in decreasing order *)
index 95f92346bcdb066e24ea9f979a8274f294cc77a8..31765f0552e8005d3c9168138a981026514dd38a 100644 (file)
@@ -269,7 +269,8 @@ let print_term ?ids_to_inner_sorts =
 
 let xml_of_attrs attributes =
   let class_of = function
-    | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+    | `Coercion n -> 
+        Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
     | `Elim s ->
         Xml.xml_nempty "class" [None,"value","elim"]
          [< Xml.xml_empty
@@ -279,9 +280,13 @@ let xml_of_attrs attributes =
     | `Record field_names ->
         Xml.xml_nempty "class" [None,"value","record"]
          (List.fold_right
-           (fun (name,coercion) res ->
+           (fun (name,coercion,arity) res ->
              [< Xml.xml_empty "field" 
-                [None,"name",if coercion then name ^ " coercion" else name]; 
+                [None,"name",
+                  if coercion then 
+                    name ^ " coercion " ^ string_of_int arity 
+                  else 
+                    name]; 
               res >]
            ) field_names [<>])
     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
index 6da6484535f53f3922ad0f735074727c02c32a3e..6cb2ad9a21fbbf4afaa16c3704c97a979daecf47 100644 (file)
@@ -499,7 +499,7 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params,attrs) ->
-       let bo' = eta_fix [] [] bo in
+       let bo' = (*eta_fix [] []*) bo in
        let ty' = eta_fix [] [] ty in
        let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
        let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
@@ -557,7 +557,7 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
            (cid,i,acanonical_context,aterm))
           conjectures' in 
 (*        let time1 = Sys.time () in *)
-       let bo' = eta_fix conjectures' [] bo in
+       let bo' = (*eta_fix conjectures' []*) bo in
        let ty' = eta_fix conjectures' [] ty in
 (*
        let time2 = Sys.time () in
index cb4d85cfd245fafb088410a89b092dd4b8375972..fbe191416a0185024ad68575688fb0bd3b91d511 100644 (file)
@@ -483,7 +483,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
      let fields' =
       snd (
        List.fold_left
-        (fun (context,res) (name,ty,_coercion) ->
+        (fun (context,res) (name,ty,_coercion,arity) ->
           let context' = Cic.Name name :: context in
            context',(name,interpretate_term context env None false ty)::res
         ) (context,[]) fields) in
@@ -500,7 +500,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
        concl fields' in
      let con' = add_params con in
      let tyl = [name,true,ty',["mk_" ^ name,con']] in
-     let field_names = List.map (fun (x,_,y) -> x,y) fields in
+     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
       Cic.InductiveDefinition
        (tyl,[],List.length params,[`Class (`Record field_names)])
   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
@@ -692,7 +692,7 @@ let domain_of_obj ~context ast =
    | CicNotationPt.Record (params,_,ty,fields) ->
       let dom =
        List.flatten
-        (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
+        (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in
       let dom =
        List.fold_left
         (fun dom (_,ty) ->
@@ -702,7 +702,7 @@ let domain_of_obj ~context ast =
        List.filter
         (fun (_,name) ->
           not (  List.exists (fun (name',_) -> name = Id name') params
-              || List.exists (fun (name',_,_) -> name = Id name') fields)
+              || List.exists (fun (name',_,_,_) -> name = Id name') fields)
         ) dom
  in
   rev_uniq domain_rev
index feca7c3cfe07951bfd32d42ff29e74f0391e976f..06bb082b4110b531209d55321e4aa9e4f4763b15 100644 (file)
@@ -80,10 +80,8 @@ let rec pp t l =
        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
     | C.Meta (n,l1) ->
        "?" ^ (string_of_int n) ^ "[" ^ 
-(*
         String.concat " ; "
          (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-*)
         "]"
     | C.Sort s ->
        (match s with
@@ -97,14 +95,14 @@ let rec pp t l =
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
-          C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
-        | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
+          C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+        | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
        )
     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
     | C.Lambda (b,s,t) ->
        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
     | C.LetIn (b,s,t) ->
-       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+       " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
     | C.Appl li ->
        "(" ^
        (List.fold_right
index 48ae522f4c9b4b170111a2dabff110e93388d863..798c38540d5118cc4f3f8ab190152d1dcfdebdd4 100644 (file)
@@ -32,8 +32,10 @@ exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 let insert_coercions = ref true
+let pack_coercions = ref true
 
 let debug_print = fun _ -> ()
+(* let debug_print x = prerr_endline (Lazy.force x);; *)
 
 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
 
@@ -123,24 +125,76 @@ let exp_impl metasenv subst context =
 
 let is_a_double_coercion t =
   let last_of l = 
-    let rec aux = function
-      | x::[] -> x
-      | x::tl -> aux tl
+    let rec aux acc = function
+      | x::[] -> acc,x
+      | x::tl -> aux (acc@[x]) tl
       | [] -> assert false
     in
-    aux l
-  in
-  let dummyres = 
-    false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None 
+    aux [] l
   in
+  let imp = Cic.Implicit None in
+  let dummyres = false,imp, imp,imp,imp in
   match t with
   | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
       (match last_of tl with
-      | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
-          let head = last_of tl2 in
-          true, c1, c2, head 
+      | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+          let sib2,head = last_of tl2 in
+          true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
+            (c2::sib2@[Cic.Implicit None])]) 
       | _ -> dummyres)
   | _ -> dummyres
+
+let more_args_than_expected subst he context hetype' tlbody_and_type =
+  lazy ("The term " ^
+    CicMetaSubst.ppterm_in_context subst he context ^ 
+    " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^
+    ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
+    " arguments that are more than expected")
+;; 
+
+let mk_prod_of_metas metasenv context' subst args = 
+  let rec mk_prod metasenv context' = function
+    | [] ->
+        let (metasenv, idx) = 
+          CicMkImplicit.mk_implicit_type metasenv subst context'
+        in
+        let irl =
+          CicMkImplicit.identity_relocation_list_for_metavariable context'
+        in
+          metasenv,Cic.Meta (idx, irl)
+    | (_,argty)::tl ->
+        let (metasenv, idx) = 
+          CicMkImplicit.mk_implicit_type metasenv subst context' 
+        in
+        let irl =
+          CicMkImplicit.identity_relocation_list_for_metavariable context'
+        in
+        let meta = Cic.Meta (idx,irl) in
+        let name =
+          (* The name must be fresh for context.                 *)
+          (* Nevertheless, argty is well-typed only in context.  *)
+          (* Thus I generate a name (name_hint) in context and   *)
+          (* then I generate a name --- using the hint name_hint *)
+          (* --- that is fresh in context'.                      *)
+          let name_hint = 
+            (* Cic.Name "pippo" *)
+            FreshNamesGenerator.mk_fresh_name ~subst metasenv 
+              (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
+              (CicMetaSubst.apply_subst_context subst context')
+              Cic.Anonymous
+              ~typ:(CicMetaSubst.apply_subst subst argty) 
+          in
+            (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+            FreshNamesGenerator.mk_fresh_name ~subst
+              [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
+        in
+        let metasenv,target =
+          mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
+        in
+          metasenv,Cic.Prod (name,meta,target)
+  in
+  mk_prod metasenv context' args
+;;
   
 let rec type_of_constant uri ugraph =
  let module C = Cic in
@@ -526,20 +580,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               type_of_aux subst metasenv context he ugraph 
             in
             let tlbody_and_type,subst'',metasenv'',ugraph2 =
-              List.fold_right
-                (fun x (res,subst,metasenv,ugraph) ->
-                   let x',ty,subst',metasenv',ugraph1 =
-                     type_of_aux subst metasenv context x ugraph
-                   in
-                    (x', ty)::res,subst',metasenv',ugraph1
-                ) tl ([],subst',metasenv',ugraph1)
+               typeof_list subst' metasenv' context ugraph1 tl
             in
-            let tl',applty,subst''',metasenv''',ugraph3 =
+            let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
               eat_prods true subst'' metasenv'' context 
                 he' hetype tlbody_and_type ugraph2
             in
-              avoid_double_coercion context 
-                subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
+            let newappl = (C.Appl (coerced_he::coerced_args)) in
+            avoid_double_coercion 
+              context subst''' metasenv''' ugraph3 newappl applty
         | C.Appl _ -> assert false
         | C.Const (uri,exp_named_subst) ->
             let exp_named_subst',subst',metasenv',ugraph1 =
@@ -816,15 +865,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
              let tlbody_and_type,subst,metasenv,ugraph4 =
-               List.fold_right
-                 (fun x (res,subst,metasenv,ugraph) ->
-                    let x',ty,subst',metasenv',ugraph1 =
-                      type_of_aux subst metasenv context x ugraph
-                    in
-                      (x', ty)::res,subst',metasenv',ugraph1
-                 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+               typeof_list subst metasenv context ugraph4 (right_args @ [term'])
              in
-             let _,_,subst,metasenv,ugraph4 =
+             let _,_,_,subst,metasenv,ugraph4 =
                eat_prods false subst metasenv context 
                  outtype outtypety tlbody_and_type ugraph4
              in
@@ -1126,7 +1169,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (CicPp.ppterm t2''))))
 
   and avoid_double_coercion context subst metasenv ugraph t ty = 
-    let b, c1, c2, head = is_a_double_coercion t in
+    let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
     if b then
       let source_carr = CoercGraph.source_of c2 in
       let tgt_carr = CicMetaSubst.apply_subst subst ty in
@@ -1135,207 +1178,326 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       | CoercGraph.SomeCoercion candidates -> 
          let selected =  
            HExtlib.list_findopt
-             (fun c ->
+             (function 
+               | c when not (CoercGraph.is_composite c) -> 
+                   debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
+                   None
+               | c ->
                let newt =
                 match c with
                 | Cic.Appl l -> Cic.Appl (l @ [head])
                 | _ -> Cic.Appl [c;head]
                in
+               debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
                (try
-                 let newt,_,subst,metasenv,ugraph = 
-                   type_of_aux subst metasenv context newt ugraph in
-                 let subst, metasenv, ugraph = 
-                  fo_unif_subst subst context metasenv newt t ugraph
-                 in
                  debug_print 
                    (lazy 
                      ("packing: " ^ 
                        CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+                 let newt,_,subst,metasenv,ugraph = 
+                   type_of_aux subst metasenv context newt ugraph in
+                 debug_print (lazy "tipa...");
+                 let subst, metasenv, ugraph =
+                   (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
+                    fo_unif_subst subst context metasenv newt t ugraph
+                 in
+                 debug_print (lazy "unifica...");
                  Some (newt, ty, subst, metasenv, ugraph)
-               with RefineFailure _ | Uncertain _ -> None))
+               with 
+               | RefineFailure s | Uncertain s when not !pack_coercions-> 
+                   debug_print s; debug_print (lazy "stop\n");None
+               | RefineFailure s | Uncertain s -> 
+                   debug_print s;debug_print (lazy "goon\n");
+                   try 
+                     pack_coercions := false; (* to avoid diverging *)
+                     let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
+                       type_of_aux subst metasenv context c1_c2_implicit ugraph 
+                     in
+                     pack_coercions := true;
+                     let b, _, _, _, _ = 
+                       is_a_double_coercion refined_c1_c2_implicit 
+                     in 
+                     if b then 
+                       None 
+                     else
+                       let head' = 
+                         match refined_c1_c2_implicit with
+                         | Cic.Appl l -> HExtlib.list_last l
+                         | _ -> assert false   
+                       in
+                       let subst, metasenv, ugraph =
+                        try fo_unif_subst subst context metasenv 
+                          head head' ugraph
+                        with RefineFailure s| Uncertain s-> 
+                          debug_print s;assert false 
+                       in
+                       let subst, metasenv, ugraph =
+                         fo_unif_subst subst context metasenv 
+                          refined_c1_c2_implicit t ugraph
+                       in
+                       Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
+                   with 
+                   | RefineFailure s | Uncertain s -> 
+                       pack_coercions := true;debug_print s;None
+                   | exn -> pack_coercions := true; raise exn))
              candidates
          in
          (match selected with
          | Some x -> x
          | None -> 
-              prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t);
-               assert false)
+              debug_print
+                (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
+              t, ty, subst, metasenv, ugraph)
       | _ -> assert false) (* the composite coercion must exist *)
     else
       t, ty, subst, metasenv, ugraph  
 
+  and typeof_list subst metasenv context ugraph l =
+    let tlbody_and_type,subst,metasenv,ugraph =
+      List.fold_right
+        (fun x (res,subst,metasenv,ugraph) ->
+           let x',ty,subst',metasenv',ugraph1 =
+             type_of_aux subst metasenv context x ugraph
+           in
+            (x', ty)::res,subst',metasenv',ugraph1
+        ) l ([],subst,metasenv,ugraph)
+    in
+      tlbody_and_type,subst,metasenv,ugraph
+
   and eat_prods 
-    allow_coercions subst metasenv context he hetype tlbody_and_type ugraph 
+    allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph 
   =
-    let rec mk_prod metasenv context' =
-      function
-          [] ->
-            let (metasenv, idx) = 
-              CicMkImplicit.mk_implicit_type metasenv subst context'
-            in
-            let irl =
-              CicMkImplicit.identity_relocation_list_for_metavariable context'
-            in
-              metasenv,Cic.Meta (idx, irl)
-        | (_,argty)::tl ->
-            let (metasenv, idx) = 
-              CicMkImplicit.mk_implicit_type metasenv subst context' 
-            in
-            let irl =
-              CicMkImplicit.identity_relocation_list_for_metavariable context'
-            in
-            let meta = Cic.Meta (idx,irl) in
-            let name =
-              (* The name must be fresh for context.                 *)
-              (* Nevertheless, argty is well-typed only in context.  *)
-              (* Thus I generate a name (name_hint) in context and   *)
-              (* then I generate a name --- using the hint name_hint *)
-              (* --- that is fresh in context'.                      *)
-              let name_hint = 
-                (* Cic.Name "pippo" *)
-                FreshNamesGenerator.mk_fresh_name ~subst metasenv 
-                  (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
-                  (CicMetaSubst.apply_subst_context subst context)
-                  Cic.Anonymous
-                  ~typ:(CicMetaSubst.apply_subst subst argty) 
-              in
-                (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
-                FreshNamesGenerator.mk_fresh_name ~subst
-                  [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
-            in
-            let metasenv,target =
-              mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
-            in
-              metasenv,Cic.Prod (name,meta,target)
-    in
-    let ((subst,metasenv,ugraph1),hetype') =
-     if CicUtil.is_meta_closed hetype then
-      (subst,metasenv,ugraph),hetype
-     else
-      let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
-       try
-         fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
-       with exn ->
-        enrich localization_tbl he
-         ~f:(fun _ ->
-           (lazy ("The term " ^
-             CicMetaSubst.ppterm_in_context subst he
-              context ^ " (that has type " ^
-             CicMetaSubst.ppterm_in_context subst hetype
-              context ^ ") is here applied to " ^
-             string_of_int (List.length tlbody_and_type) ^
-             " arguments that are more than expected"
-              (* "\nReason: " ^ Lazy.force exn*)))) exn
+    (* aux function to add coercions to funclass *)
+    let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
+      (* {{{ body *)
+      let pristinemenv = metasenv in
+      let metasenv,hetype' = 
+        mk_prod_of_metas metasenv context subst args_bo_and_ty 
+      in
+      try
+        let subst,metasenv,ugraph = 
+          fo_unif_subst_eat_prods 
+            subst context metasenv hetype hetype' ugraph
+        in
+        subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+      with RefineFailure s | Uncertain s as exn 
+      when allow_coercions && !insert_coercions ->
+        (* {{{ we search a coercion of the head (saturated) to funclass *)
+        let metasenv = pristinemenv in
+        debug_print (lazy 
+          ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
+           " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^ 
+           " cause: " ^ Lazy.force s));
+        let how_many_args_are_needed = 
+          let rec aux n = function
+            | Cic.Prod(_,_,t) -> aux (n+1) t
+            | _ -> n
+          in
+          aux 0 (CicMetaSubst.apply_subst subst hetype)
+        in
+        let args, remainder = 
+          HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
+        in
+        let args = List.map fst args in
+        let x = 
+          if args <> [] then 
+            match he with
+            | Cic.Appl l -> Cic.Appl (l@args)
+            | _ -> Cic.Appl (he::args) 
+          else
+            he
+        in
+        let x,xty,subst,metasenv,ugraph =
+            type_of_aux subst metasenv context x ugraph
+        in
+        let carr_src = 
+          CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) 
+        in
+        let carr_tgt = CoercDb.Fun 0 in
+        match CoercGraph.look_for_coercion' carr_src carr_tgt with
+        | CoercGraph.NoCoercion 
+        | CoercGraph.NotMetaClosed 
+        | CoercGraph.NotHandled _ -> raise exn
+        | CoercGraph.SomeCoercion candidates ->
+            match  
+            HExtlib.list_findopt 
+              (fun coerc -> 
+                let t = Cic.Appl [coerc;x] in
+                debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
+                try
+                  (* we want this to be available in the error handler fo the
+                   * following (so it has its own try. *)
+                  let t,tty,subst,metasenv,ugraph =
+                    type_of_aux subst metasenv context t ugraph
+                  in 
+                  try
+                    let metasenv, hetype' = 
+                      mk_prod_of_metas metasenv context subst remainder 
+                    in
+                    debug_print (lazy 
+                      ("  unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ 
+                       CicMetaSubst.ppterm subst hetype'));
+                    let subst,metasenv,ugraph = 
+                      fo_unif_subst_eat_prods 
+                        subst context metasenv tty hetype' ugraph
+                    in
+                    debug_print (lazy " success!");
+                    Some (subst,metasenv,ugraph,tty,t,remainder) 
+                  with 
+                  | Uncertain _ | RefineFailure _
+                  | CicUnification.UnificationFailure _ 
+                  | CicUnification.Uncertain _ -> 
+                      try 
+                        let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
+                          fix_arity
+                            metasenv context subst t tty remainder ugraph
+                        in
+                        Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
+                      with exn -> None
+                with exn -> None)
+              candidates
+           with
+           | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
+               subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+           | None -> 
+               enrich localization_tbl he
+                ~f:(fun _-> more_args_than_expected subst he context hetype
+                             args_bo_and_ty) exn
+      (* }}} end coercion to funclass stuff *)           
+      (* }}} end fix_arity *)           
     in
-    let rec eat_prods metasenv subst context hetype ugraph =
+    (* aux function to process the type of the head and the args in parallel *)
+    let rec eat_prods_and_args 
+      pristinemenv metasenv subst context he hetype ugraph newargs 
+    =
+      (* {{{ body *)
       function
-        | [] -> [],metasenv,subst,hetype,ugraph
+        | [] -> newargs,subst,metasenv,he,hetype,ugraph
         | (hete, hety)::tl ->
-           (match (CicReduction.whd ~subst context hetype) with 
-                 Cic.Prod (n,s,t) ->
-                   let arg,subst,metasenv,ugraph1 =
-                     try
-                       let subst,metasenv,ugraph1 = 
-                         fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph
-                       in
-                         hete,subst,metasenv,ugraph1
-                     with exn when allow_coercions && !insert_coercions ->
-                       (* we search a coercion from hety to s *)
-                       let coer, tgt_carr = 
-                         let carr t subst context = 
-                           CicReduction.whd ~delta:false 
-                             context (CicMetaSubst.apply_subst subst t )
-                         in
-                         let c_hety = carr hety subst context in
-                         let c_s = carr s subst context in 
-                         CoercGraph.look_for_coercion c_hety c_s, c_s
-                       in
-                       (match coer with
-                       | CoercGraph.NoCoercion 
-                       | CoercGraph.NotHandled _ ->
-                           enrich localization_tbl hete
-                            (RefineFailure
-                              (lazy ("The term " ^
-                                CicMetaSubst.ppterm_in_context subst hete
-                                 context ^ " has type " ^
-                                CicMetaSubst.ppterm_in_context subst hety
-                                 context ^ " but is here used with type " ^
-                                CicMetaSubst.ppterm_in_context subst s context
-                                 (* "\nReason: " ^ Lazy.force e*))))
-                       | CoercGraph.NotMetaClosed -> 
-                           enrich localization_tbl hete
-                            (Uncertain
-                              (lazy ("The term " ^
-                                CicMetaSubst.ppterm_in_context subst hete
-                                 context ^ " has type " ^
-                                CicMetaSubst.ppterm_in_context subst hety
-                                 context ^ " but is here used with type " ^
-                                CicMetaSubst.ppterm_in_context subst s context
-                                 (* "\nReason: " ^ Lazy.force e*))))
-                       | CoercGraph.SomeCoercion candidates -> 
-                           let selected = 
-                             HExtlib.list_findopt
-                               (fun c -> 
-                                try
-                                 let t = Cic.Appl[c;hete] in
-                                 let newt,newhety,subst,metasenv,ugraph = 
-                                  type_of_aux subst metasenv context
-                                   t ugraph 
-                                 in
-                                 let newt, _, subst, metasenv, ugraph = 
-                                  avoid_double_coercion context subst metasenv
-                                   ugraph newt tgt_carr 
-                                 in
-                                 let subst,metasenv,ugraph1 = 
-                                   fo_unif_subst subst context metasenv 
-                                      newhety s ugraph
-                                 in
-                                  Some (newt, subst, metasenv, ugraph)
-                                with Uncertain _ | RefineFailure _ -> None)
-                               candidates
-                           in
-                           (match selected with
-                           | Some x -> x
-                           | None ->  
-                              enrich localization_tbl hete
-                               ~f:(fun _ ->
-                                (lazy ("The term " ^
-                                 CicMetaSubst.ppterm_in_context subst hete
-                                  context ^ " has type " ^
-                                 CicMetaSubst.ppterm_in_context subst hety
-                                  context ^ " but is here used with type " ^
-                                 CicMetaSubst.ppterm_in_context subst s context
-                                  (* "\nReason: " ^ Lazy.force e*)))) exn))
-                     | exn ->
+            match (CicReduction.whd ~subst context hetype) with 
+            | Cic.Prod (n,s,t) ->
+                let arg,subst,metasenv,ugraph1 =
+                  try
+                    let subst,metasenv,ugraph1 = 
+                      fo_unif_subst_eat_prods2 
+                        subst context metasenv hety s ugraph
+                    in
+                      (hete,hety),subst,metasenv,ugraph1
+                  (* {{{ we search a coercion from hety to s if fails *)
+                  with RefineFailure _ | Uncertain _ as exn 
+                  when allow_coercions && !insert_coercions ->
+                    let coer, tgt_carr = 
+                      let carr t subst context = 
+                        CicReduction.whd ~delta:false 
+                          context (CicMetaSubst.apply_subst subst t )
+                      in
+                      let c_hety = carr hety subst context in
+                      let c_s = carr s subst context in 
+                      CoercGraph.look_for_coercion c_hety c_s, c_s
+                    in
+                    (match coer with
+                    | CoercGraph.NoCoercion 
+                    | CoercGraph.NotHandled _ ->
                         enrich localization_tbl hete
-                         ~f:(fun _ ->
+                         (RefineFailure
                            (lazy ("The term " ^
                              CicMetaSubst.ppterm_in_context subst hete
                               context ^ " has type " ^
                              CicMetaSubst.ppterm_in_context subst hety
                               context ^ " but is here used with type " ^
                              CicMetaSubst.ppterm_in_context subst s context
-                              (* "\nReason: " ^ Lazy.force e*)))) exn
-                   in
-                   let coerced_args,metasenv',subst',t',ugraph2 =
-                     eat_prods metasenv subst context
-                       (CicSubstitution.subst arg t) ugraph1 tl
-                   in
-                     arg::coerced_args,metasenv',subst',t',ugraph2
-               | _ ->
-                 raise (RefineFailure
-                  (lazy ("The term " ^
-                    CicMetaSubst.ppterm_in_context subst he
-                     context ^ " (that has type " ^
-                    CicMetaSubst.ppterm_in_context subst hetype'
-                     context ^ ") is here applied to " ^
-                    string_of_int (List.length tlbody_and_type) ^
-                    " arguments that are more than expected"))))
+                              (* "\nReason: " ^ Lazy.force e*))))
+                    | CoercGraph.NotMetaClosed -> 
+                        enrich localization_tbl hete
+                         (Uncertain
+                           (lazy ("The term " ^
+                             CicMetaSubst.ppterm_in_context subst hete
+                              context ^ " has type " ^
+                             CicMetaSubst.ppterm_in_context subst hety
+                              context ^ " but is here used with type " ^
+                             CicMetaSubst.ppterm_in_context subst s context
+                              (* "\nReason: " ^ Lazy.force e*))))
+                    | CoercGraph.SomeCoercion candidates -> 
+                        let selected = 
+                          HExtlib.list_findopt
+                            (fun c -> 
+                             try
+                              let t = Cic.Appl[c;hete] in
+                              let newt,newhety,subst,metasenv,ugraph = 
+                               type_of_aux subst metasenv context
+                                t ugraph 
+                              in
+                              let newt, newty, subst, metasenv, ugraph = 
+                               avoid_double_coercion context subst metasenv
+                                ugraph newt tgt_carr 
+                              in
+                              let subst,metasenv,ugraph1 = 
+                                fo_unif_subst subst context metasenv 
+                                   newhety s ugraph
+                              in
+                               Some ((newt,newty), subst, metasenv, ugraph)
+                             with Uncertain _ | RefineFailure _ -> None)
+                            candidates
+                        in
+                        (match selected with
+                        | Some x -> x
+                        | None ->  
+                           enrich localization_tbl hete
+                            ~f:(fun _ ->
+                             (lazy ("The term " ^
+                              CicMetaSubst.ppterm_in_context subst hete
+                               context ^ " has type " ^
+                              CicMetaSubst.ppterm_in_context subst hety
+                               context ^ " but is here used with type " ^
+                              CicMetaSubst.ppterm_in_context subst s context
+                               (* "\nReason: " ^ Lazy.force e*)))) exn))
+                  | exn ->
+                     enrich localization_tbl hete
+                      ~f:(fun _ ->
+                        (lazy ("The term " ^
+                          CicMetaSubst.ppterm_in_context subst hete
+                           context ^ " has type " ^
+                          CicMetaSubst.ppterm_in_context subst hety
+                           context ^ " but is here used with type " ^
+                          CicMetaSubst.ppterm_in_context subst s context ^
+                           "\nReason: " ^ Printexc.to_string exn))) exn
+                  (* }}} end coercion stuff *)
+                in
+                  eat_prods_and_args pristinemenv metasenv subst context he
+                    (CicSubstitution.subst (fst arg) t) 
+                    ugraph1 (newargs@[arg]) tl
+            | _ -> 
+                try
+                  let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
+                    fix_arity 
+                      pristinemenv context subst he hetype 
+                       (newargs@[hete,hety]@tl) ugraph
+                  in
+                  eat_prods_and_args metasenv
+                    metasenv subst context he hetype' ugraph [] args_bo_and_ty
+                with RefineFailure s | Uncertain s ->
+                  (* unable to fix arity *)
+                  let msg = 
+                   more_args_than_expected 
+                     subst he context hetype args_bo_and_ty
+                  in
+                  raise (RefineFailure msg)
+      (* }}} *)
+    in
+    (* first we check if we are in the simple case of a meta closed term *)
+    let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
+     if CicUtil.is_meta_closed hetype then
+      (* this optimization is to postpone fix_arity (the most common case)*)
+      subst,metasenv,ugraph,hetype,he,args_bo_and_ty
+     else
+       (* this (says CSC) is also useful to infer dependent types *)
+       fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
     in
-    let coerced_args,metasenv,subst,t,ugraph2 =
-      eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type 
+    let coerced_args,subst,metasenv,he,t,ugraph =
+      eat_prods_and_args 
+        metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
     in
-      coerced_args,t,subst,metasenv,ugraph2
+    he,(List.map fst coerced_args),t,subst,metasenv,ugraph
   in
   
   (* eat prods ends here! *)
@@ -1566,7 +1728,7 @@ let pack_coercion metasenv ctx t =
    | C.Appl l -> 
       let l = List.map (merge_coercions ctx) l in
       let t = C.Appl l in
-       let b,_,_,_ = is_a_double_coercion t in
+       let b,_,_,_,_ = is_a_double_coercion t in
        (* prerr_endline "CANDIDATO!!!!"; *)
        if b then
          let ugraph = CicUniv.empty_ugraph in
@@ -1721,3 +1883,4 @@ let typecheck ~localization_tbl metasenv uri obj =
  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
 
 let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
+(* vim:set foldmethod=marker: *)
index 44712199e412b370170b8753c6aa0e488d6a12bf..ecde4cdfd9bd2fb1dee201d64f96c75f8437a9ce 100644 (file)
@@ -578,13 +578,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                 fo_unif_l 
                   test_equality_only subst metasenv (lr1, lr2)  ugraph
               with 
-              | UnificationFailure _
-              | Uncertain _ as exn -> 
+              | UnificationFailure s
+              | Uncertain s as exn -> 
                   (match l1, l2 with
                   | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
                      (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
                     CoercGraph.is_a_coercion c1 && 
-                    CoercGraph.is_a_coercion c2 ->
+                    CoercGraph.is_a_coercion c2 &&
+                    not (UriManager.eq uri1 uri2) ->
                       let body1, attrs1, ugraph = 
                         match CicEnvironment.get_obj ugraph uri1 with
                         | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo,attrs,u
@@ -596,9 +597,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                         | _ -> assert false
                       in
                       let is_composite1 = 
-                        List.exists ((=) (`Class `Coercion)) attrs1 in
+                        List.exists 
+                         (function `Class (`Coercion _) -> true | _-> false) 
+                         attrs1 
+                      in
                       let is_composite2 = 
-                        List.exists ((=) (`Class `Coercion)) attrs2 in
+                        List.exists 
+                         (function `Class (`Coercion _) -> true | _-> false) 
+                         attrs2 
+                      in
                       (match is_composite1, is_composite2 with
                       | false, false -> raise exn
                       | true, false ->
index bd82a603c1bad2340f31b5601a2f4994c499772f..c076e9f9671e54277b7b009e9b9ec78a286241c3 100644 (file)
@@ -10,6 +10,10 @@ hLog.cmo: hLog.cmi
 hLog.cmx: hLog.cmi 
 trie.cmo: trie.cmi 
 trie.cmx: trie.cmi 
+trie.cmo: trie.cmi 
+trie.cmx: trie.cmi 
+hTopoSort.cmo: hTopoSort.cmi 
+hTopoSort.cmx: hTopoSort.cmi 
 refCounter.cmo: refCounter.cmi 
 refCounter.cmx: refCounter.cmi 
 graphvizPp.cmo: graphvizPp.cmi 
index 25b49280c29cde8883bc688fd32ffdc10b2fe7b4..f4d92191df82b0429c0e4648755ba1a3956aeafd 100644 (file)
@@ -8,6 +8,7 @@ INTERFACE_FILES =               \
        patternMatcher.mli      \
        hLog.mli                \
        trie.mli                \
+       hTopoSort.mli           \
        refCounter.mli          \
        graphvizPp.mli          \
        $(NULL)
index 4804699e0a7ef048dae9851641411e7e768be6e5..82fa9807de15a786b8bd7e338ca82af3348976e5 100644 (file)
@@ -30,6 +30,7 @@ type attribute = string * string  (* <key, value> pair *)
 module type GraphvizFormatter =
   sig
     val header:
+      ?graph_type:string -> 
       ?name:string -> ?graph_attrs:(attribute list) ->
       ?node_attrs:(attribute list) -> ?edge_attrs:(attribute list) ->
       Format.formatter ->
@@ -55,8 +56,8 @@ module Dot =
       attributes attrs fmt;
       fprintf fmt "];@]@,"
 
-    let header ?(name = "g") ?(graph_attrs = []) ?node_attrs ?edge_attrs fmt =
-      fprintf fmt "@[<hv2>strict digraph %s {@," name;
+    let header ?(graph_type = "digraph") ?(name = "g") ?(graph_attrs = []) ?node_attrs ?edge_attrs fmt =
+      fprintf fmt "@[<hv2>%s %s {@," graph_type name;
       List.iter (fun (k, v) -> fprintf fmt "@[<hv2>%s=@,%s;@]@," k v)
         graph_attrs;
       (match node_attrs with
index a10831dca7f959d2454973bed2e097ac7d77ec2d..79037df7283cc717d8282d465db3f17c56980d75 100644 (file)
@@ -32,10 +32,13 @@ type attribute = string * string  (* <key, value> pair *)
 module type GraphvizFormatter =
   sig
     (** @param name graph name
+     * @param graph_type type of dot graph, default value "digraph"
+     *        interesting options: "strict digraph"
      * @param graph_attrs graph attributes
      * @param node_attrs graph-wide node attributes
      * @param edge_attrs graph-wide edge attributes *)
     val header:
+      ?graph_type:string -> 
       ?name:string -> ?graph_attrs:(attribute list) ->
       ?node_attrs:(attribute list) -> ?edge_attrs:(attribute list) ->
       Format.formatter ->
index 3cc6c9bb5c0bc876f74d35de8868f3231a56c14e..c0364315a62c018923f2c9e76873a35087c15fd2 100644 (file)
@@ -180,6 +180,11 @@ let split_nth n l =
     | n, hd :: tl -> aux (hd :: acc) (n - 1) tl in
   aux [] n l
 
+let list_last l =
+  let l = List.rev l in 
+  try List.hd l with exn -> raise (Failure "HExtlib.list_last")
+;;
+  
 (** {2 File predicates} *)
 
 let is_dir fname =
index 8de41f6837df4a067bab010438a8731a81d35b88..0c2206a08bd82339f85cb3ad8c60934b9fcb0aba 100644 (file)
@@ -78,6 +78,7 @@ val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *)
 val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*)
 val list_findopt: ('a -> 'b option) -> 'a list -> 'b option
 val flatten_map: ('a -> 'b list) -> 'a list -> 'b list
+val list_last: 'a list -> 'a
 
   (** split_nth n l
    * @returns two list, the first contains at least n elements, the second the
diff --git a/components/extlib/hTopoSort.ml b/components/extlib/hTopoSort.ml
new file mode 100644 (file)
index 0000000..cc593d5
--- /dev/null
@@ -0,0 +1,69 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+module Make (OT:Map.OrderedType) =
+    struct
+      
+      module M = Map.Make(OT);;
+      
+      let topological_sort l find_deps = 
+        let find_deps m x = 
+          let deps = find_deps x in
+          M.add x deps m
+        in
+        (* build the partial order relation *)
+        let m = List.fold_left (fun m i -> find_deps m i) M.empty l in
+        let m = (* keep only deps inside l *) 
+          List.fold_left 
+            (fun m' i ->
+              M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m') 
+            M.empty l 
+        in
+        let m = M.map (fun x -> Some x) m in
+        (* utils *)
+        let keys m = M.fold (fun i _ acc -> i::acc) m [] in
+        let split l m = List.filter (fun i -> M.find i m = Some []) l in
+        let purge l m = 
+          M.mapi 
+            (fun k v -> if List.mem k l then None else 
+               match v with
+               | None -> None
+               | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) 
+            m
+        in
+        let rec aux m res = 
+            let keys = keys m in
+            let ok = split keys m in
+            let m = purge ok m in
+            let res = ok @ res in
+            if ok = [] then res else aux m res
+        in
+        let rc = List.rev (aux m []) in
+        rc
+      ;;
+      
+    end
+;;
+
diff --git a/components/extlib/hTopoSort.mli b/components/extlib/hTopoSort.mli
new file mode 100644 (file)
index 0000000..5cd15fb
--- /dev/null
@@ -0,0 +1,32 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+module Make :
+  functor (OT : Map.OrderedType) ->
+    sig
+      module M : Map.S with type key = OT.t
+      val topological_sort :
+        M.key list -> (M.key -> M.key list) -> M.key list
+    end
index b4c18726cd4ca73c36389f4521bc47ad3cb49a6b..b516d393e12c123d3a539353fb83b62cc0ef211d 100644 (file)
@@ -118,7 +118,7 @@ type 'term macro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 8
+let magic = 9
 
 type 'obj command =
   | Default of loc * string * UriManager.uri list
@@ -127,7 +127,7 @@ type 'obj command =
   | Drop of loc
   | Print of loc * string
   | Qed of loc
-  | Coercion of loc * UriManager.uri * bool (* add composites *)
+  | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *)
   | Obj of loc * 'obj
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactical =
index c7db02872afd57942400a84f75b831ada92c409c..b78f6d90b5999c97646f88430f01d2f3be140c7f 100644 (file)
@@ -218,8 +218,8 @@ let pp_default what uris =
   sprintf "default \"%s\" %s" what
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
-let pp_coercion uri do_composites =
-   sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
+let pp_coercion uri do_composites arity =
+   sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
      (if do_composites then "compounds" else "no compounds")
     
 let pp_command ~obj_pp = function
@@ -228,7 +228,7 @@ let pp_command ~obj_pp = function
   | Drop _ -> "drop"
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-  | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
+  | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
   | Obj (_,obj) -> obj_pp obj
   | Default (_,what,uris) ->
       pp_default what uris
index e786d500154f4747b0128bdcf323178793278244..2b1ed9dbaafb6765e1acc78f04b4770fcc1b4e6e 100644 (file)
@@ -44,8 +44,8 @@ let rehash_cmd_uris =
   | GrafiteAst.Default (loc, name, uris) ->
       let uris = List.map rehash_uri uris in
       GrafiteAst.Default (loc, name, uris)
-  | GrafiteAst.Coercion (loc, uri, close) ->
-      GrafiteAst.Coercion (loc, rehash_uri uri, close)
+  | GrafiteAst.Coercion (loc, uri, close, arity) ->
+      GrafiteAst.Coercion (loc, rehash_uri uri, close, arity)
   | cmd ->
       prerr_endline "Found a command not expected in a .moo:";
       let obj_pp _ = assert false in
index 9e524b377fc68e2cb300d2efb13b871b74551894..2de83bc4078b569613b2b922fc9dc0e791ba75a2 100644 (file)
@@ -414,8 +414,8 @@ type 'a eval_executable =
 type 'a eval_from_moo =
  { efm_go: GT.status -> string -> GT.status }
       
-let coercion_moo_statement_of uri =
-  GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
+let coercion_moo_statement_of arity uri =
+  GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity)
 
 let refinement_toolkit = {
   RefinementTool.type_of_aux' = 
@@ -440,11 +440,12 @@ let refinement_toolkit = {
   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
  }
   
-let eval_coercion status ~add_composites uri =
+let eval_coercion status ~add_composites uri arity =
  let status,compounds =
-  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
+  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity 
+ in
  let moo_content = 
-   List.map coercion_moo_statement_of (uri::compounds)
+   List.map (coercion_moo_statement_of arity) (uri::compounds)
  in
  let status = GT.add_moo_content moo_content status in
   {status with GT.proof_status = GT.No_proof},
@@ -551,7 +552,11 @@ let add_coercions_of_record_to_moo obj lemmas status =
           let obj,_ = 
             CicEnvironment.get_cooked_obj  CicUniv.empty_ugraph uri in
           let attrs = CicUtil.attributes_of_obj obj in
-          List.mem (`Class `Coercion) attrs
+          try 
+            match List.find 
+             (function `Class (`Coercion _) -> true | _-> false) attrs
+            with `Class (`Coercion n) -> true,n | _ -> assert false
+          with Not_found -> false,0            
         with Not_found -> assert false
       in
       (* looking at the fields we can know the 'wanted' coercions, but not the 
@@ -561,9 +566,9 @@ let add_coercions_of_record_to_moo obj lemmas status =
       let wanted_coercions = 
         HExtlib.filter_map 
           (function 
-            | (name,true) -> 
+            | (name,true,arity) -> 
                Some 
-                 (UriManager.uri_of_string 
+                 (arity, UriManager.uri_of_string 
                    (GT.qualify status name ^ ".con"))
             | _ -> None) 
           fields
@@ -576,13 +581,22 @@ let add_coercions_of_record_to_moo obj lemmas status =
         List.split
           (HExtlib.filter_map 
             (fun uri ->
-              let is_a_wanted_coercion = 
-                List.exists (UriManager.eq uri) wanted_coercions 
+              let is_a_wanted_coercion,arity_wanted = 
+                try
+                  let arity,_ = 
+                    List.find (fun (n,u) -> UriManager.eq u uri) 
+                      wanted_coercions
+                  in
+                  true, arity
+                with Not_found -> false, 0
               in
-              if is_a_coercion uri || is_a_wanted_coercion then
-                Some (uri, coercion_moo_statement_of uri)
+              let is_a_coercion, arity_coercion = is_a_coercion uri in
+              if is_a_coercion then
+                Some (uri, coercion_moo_statement_of arity_coercion uri)
+              else if is_a_wanted_coercion then
+                Some (uri, coercion_moo_statement_of arity_wanted uri)
               else
-                None) 
+                None)
             lemmas)
       in
       (*prerr_endline "actual coercions:";
@@ -681,8 +695,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let status, lemmas = add_obj uri obj status in
        {status with GT.proof_status = GT.No_proof},
         uri::lemmas
-  | GrafiteAst.Coercion (loc, uri, add_composites) ->
-     eval_coercion status ~add_composites uri
+  | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
+     eval_coercion status ~add_composites uri arity
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with
index 4809bd2e5d833d5261d6330f8b9834ded61e2020..7b4bdfb5e5c04f43bfc44ccd11debbb28cf5a04e 100644 (file)
@@ -32,8 +32,9 @@ let add_obj refinement_toolkit uri obj status =
   {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
    lemmas
 
-let add_coercion refinement_toolkit ~add_composites status uri =
- let compounds = LibrarySync.add_coercion ~add_composites refinement_toolkit uri in
+let add_coercion refinement_toolkit ~add_composites status uri arity =
+ let compounds = 
+   LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity in
   {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
    compounds
  
index 5e384a47ac607b0eb82ca4d5ed2c63dd8ced51ab..8453dd64559c994627348c13389d957698e88c99 100644 (file)
@@ -31,7 +31,7 @@ val add_obj:
 val add_coercion:
   RefinementTool.kit ->
   add_composites:bool -> GrafiteTypes.status ->
-  UriManager.uri -> 
+  UriManager.uri -> int ->
     GrafiteTypes.status * UriManager.uri list
 
 val time_travel: 
index c4e12ac080a18a1786c7efbf9cdd9a0dab9a9a40..9373e54b43a1de051f743a2581220677abaf4df8 100644 (file)
@@ -386,8 +386,14 @@ EXTEND
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
        name = IDENT ; 
-       coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; 
-       ty = term -> (name,ty,coercion) 
+       coercion = [ 
+           SYMBOL ":" -> false,0 
+         | SYMBOL ":"; SYMBOL ">" -> true,0
+         | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
+       ]; 
+       ty = term -> 
+         let b,n = coercion in 
+         (name,ty,b,n) 
      ] SEP SYMBOL ";"; SYMBOL "}" -> 
       let params =
         List.fold_right
@@ -561,8 +567,9 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ->
-        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+        let arity = match arity with None -> 0 | Some x -> x in
+        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
index 9fb188d486bfd15cdbd177af975c47e67e4892ff..65bb7ce64657b7a805af49feb64259175972f8b1 100644 (file)
@@ -36,7 +36,7 @@ type alias_spec =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 5
+let magic = 6
 
 type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
 
index 9a9ddb62bd6e797a89eed53de5e96997a5b76a8a..33309f109e6c48d2b9f11b5885170ac4d65bab8c 100644 (file)
@@ -43,12 +43,12 @@ let get_closure_coercions src tgt uri coercions =
   | CoercDb.Uri _, CoercDb.Uri _ ->
       let c_from_tgt = 
         List.filter 
-          (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src)) 
+          (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) 
           coercions 
       in
       let c_to_src = 
         List.filter 
-          (fun (f,t,_) -> eq_carr t src && not (eq_carr f tgt)) 
+          (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) 
           coercions 
       in
         (HExtlib.flatten_map 
@@ -70,31 +70,37 @@ let get_closure_coercions src tgt uri coercions =
   | _ -> [] (* do not close in case source or target is not an indty ?? *)
 ;;
 
-let obj_attrs = [`Class `Coercion; `Generated]
+let obj_attrs n = [`Class (`Coercion n); `Generated]
 
 exception UnableToCompose
 
 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
-let generate_composite_closure rt c1 c2 univ =
+let generate_composite_closure rt c1 c2 univ arity =
   let module RT = RefinementTool in
   let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
   let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in
-  let rec mk_implicits n =
-    match n with 
-    | 0 -> []
-    | _ -> (Cic.Implicit None) :: mk_implicits (n-1)
+  let rec mk_implicits = function
+    | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
   in
-  let rec mk_lambda_spline c = function
+  let rec mk_lambda_spline c namer = function
     | 0 -> c
     | n -> 
         Cic.Lambda 
-          (Cic.Name ("A" ^ string_of_int (n-1)), 
+          (namer n,
            (Cic.Implicit None), 
-           mk_lambda_spline c (n-1))
+           mk_lambda_spline c namer (n-1))
   in 
-  let rec count_saturations_needed n = function
-    | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t
-    | _ -> n
+  let count_saturations_needed t arity = 
+    let rec aux acc n = function
+      | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> 
+          aux (acc@[name]) (n+1) t
+      | _ -> n,acc
+    in
+    let len,names = aux [] 0 t in
+    let len = len - arity in
+    List.fold_left 
+      (fun (n,l) x -> if n <= len then n+1,l@[x] else n,l) (0,[]) 
+      names
   in
   let compose c1 nc1 c2 nc2 =
     Cic.Lambda 
@@ -103,11 +109,21 @@ let generate_composite_closure rt c1 c2 univ =
       Cic.Appl ( c2 :: mk_implicits nc2 @ 
         [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ]))
   in
+(*
   let order_metasenv metasenv = 
-    List.sort 
-      (fun (_,ctx1,_) (_,ctx2,_) -> List.length ctx1 - List.length ctx2) 
-      metasenv
+    let module OT = struct type t = int let compare = Pervasives.compare end in
+    let module S = HTopoSort.Make (OT) in
+    let dep i = 
+      let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
+      let metas = List.map fst (CicUtil.metas_of_term ty) in
+      HExtlib.list_uniq (List.sort Pervasives.compare metas)
+    in
+    let om =  
+      S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep 
+    in
+    List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om
   in 
+*)
   let rec create_subst_from_metas_to_rels n = function 
     | [] -> []
     | (metano, ctx, ty)::tl -> 
@@ -128,26 +144,77 @@ let generate_composite_closure rt c1 c2 univ =
     in
     aux t
   in
+  let order_body_menv term body_metasenv =
+    let rec purge_lambdas = function
+      | Cic.Lambda (_,_,t) -> purge_lambdas t
+      | t -> t
+    in
+    let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
+    let metas_that_saturate l =
+      List.fold_left 
+        (fun (acc,n) t ->
+          let metas = CicUtil.metas_of_term t in
+          let metas = List.map fst metas in
+          let metas = 
+            List.filter 
+              (fun i -> List.for_all (fun (j,_) -> j<>i) acc) 
+              metas 
+          in
+          let metas = List.map (fun i -> i,n) metas in
+          metas @ acc, n+1)
+        ([],0) l
+    in
+    let l_c2 = skip_appl (purge_lambdas term) in
+    let l_c1 = 
+      match HExtlib.list_last l_c2 with
+      | Cic.Appl l -> List.tl l
+      | _ -> assert false
+    in
+    (* i should cut off the laet elem of l_c2 *)
+    let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
+    List.sort 
+      (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
+          try List.assoc i meta2no -  List.assoc j meta2no 
+          with Not_found -> assert false) 
+      body_metasenv
+  in
+  let namer l n = 
+    let l = List.map (function Cic.Name s -> s | _ -> "A") l in
+    let l = List.fold_left
+      (fun acc s -> 
+        let rec add' s =
+          if List.exists ((=) s) acc then add' (s^"'") else s
+        in
+        acc@[add' s])
+      [] l
+    in
+    let l = List.rev l in 
+    Cic.Name (List.nth l (n-1))
+  in 
   debug_print (lazy ("\nCOMPOSING"));
   debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
   debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
-  let saturations_for_c1 = count_saturations_needed 0 c1_ty in 
-  let saturations_for_c2 = count_saturations_needed 0 c2_ty in
+  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty arity in 
+  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty 0 in
   let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
   let spline_len = saturations_for_c1 + saturations_for_c2 in
-  let c = mk_lambda_spline c spline_len in
-  (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *)
+  let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
+  debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
   let c, univ = 
     match rt.RT.type_of_aux' [] [] c univ with
     | RT.Success (term, ty, metasenv, ugraph) -> 
         debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
-        let metasenv = order_metasenv metasenv in
-        debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv));
+(*         let metasenv = order_metasenv metasenv in *)
+(*         debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv)); *)
         let body_metasenv, lambdas_metasenv = 
           split_metasenv metasenv spline_len 
         in
+(*
         debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
         debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv));
+*)
+        let body_metasenv = order_body_menv term body_metasenv in
+        debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
         let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
         debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
         let term = rt.RT.apply_subst subst term in
@@ -174,7 +241,7 @@ let generate_composite_closure rt c1 c2 univ =
   let cleaned_ty =
     FreshNamesGenerator.clean_dummy_dependent_types c_ty 
   in
-  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in 
+  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in 
     obj,univ
 ;;
 
@@ -201,26 +268,33 @@ let mangle s t l =
 
 exception ManglingFailed of string 
 
-let number_if_already_defined buri name =
+let number_if_already_defined buri name l =
+  let err () =
+    raise 
+      (ManglingFailed 
+        ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con"))
+  in
   let rec aux n =
     let suffix = if n > 0 then string_of_int n else "" in
-    let uri = buri ^ "/" ^ name ^ suffix ^ ".con" in
-    try
-      let _  = Http_getter.resolve ~writable:true uri in
-      if Http_getter.exists uri then
+    let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in
+    let uri = UriManager.uri_of_string suri in
+    let retry () = 
+      if n < 100 then 
         begin
-          HLog.warn ("Uri " ^ uri ^ " already exists.");
-          if n < 10 then aux (n+1) else 
-            raise 
-              (ManglingFailed 
-                ("Unable to give an altenative name to " ^ 
-                  buri ^ "/" ^ name ^ ".con"))
+          HLog.warn ("Uri " ^ suri ^ " already exists.");
+          aux (n+1)
         end
       else
-        UriManager.uri_of_string uri
-    with 
-    | Http_getter_types.Key_not_found _ -> UriManager.uri_of_string uri
-    | Http_getter_types.Unresolvable_URI _ -> assert false
+        err ()
+    in
+    if List.exists (UriManager.eq uri) l then retry ()
+    else
+      try
+        let _  = Http_getter.resolve' ~writable:true uri in
+        if Http_getter.exists' uri then retry () else uri
+      with 
+      | Http_getter_types.Key_not_found _ -> uri
+      | Http_getter_types.Unresolvable_URI _ -> assert false
   in
   aux 0
 ;;
@@ -235,23 +309,24 @@ let close_coercion_graph rt src tgt uri =
   let todo_list = filter_duplicates todo_list coercions in
   try
     let new_coercions = 
-      HExtlib.filter_map (
-        fun (src, l , tgt) ->
+      List.fold_left (
+        fun acc (src, l , tgt) ->
           try 
             (match l with
             | [] -> assert false 
             | he :: tl ->
+                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
                 let first_step = 
                   Cic.Constant ("", 
                     Some (CoercDb.term_of_carr (CoercDb.Uri he)),
-                    Cic.Sort Cic.Prop, [], obj_attrs)
+                    Cic.Sort Cic.Prop, [], obj_attrs arity)
                 in
                 let o,_ = 
                   List.fold_left (fun (o,univ) coer ->
                     match o with 
                     | Cic.Constant (_,Some c,_,[],_) ->
-                          generate_composite_closure rt c 
-                            (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
+                        generate_composite_closure rt c 
+                          (CoercDb.term_of_carr (CoercDb.Uri coer)) univ arity
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl
                 in
@@ -260,16 +335,19 @@ let close_coercion_graph rt src tgt uri =
                 let by = List.map UriManager.name_of_uri l in
                 let name = mangle name_tgt name_src by in
                 let buri = UriManager.buri_of_uri uri in
-                let c_uri = number_if_already_defined buri name in
+                let c_uri = 
+                  number_if_already_defined buri name 
+                    (List.map (fun (_,_,u,_) -> u) acc) 
+                in
                 let named_obj = 
                   match o with
                   | Cic.Constant (_,bo,ty,vl,attrs) ->
                       Cic.Constant (name,bo,ty,vl,attrs)
                   | _ -> assert false 
                 in
-                  Some ((src,tgt,c_uri,named_obj)))
-          with UnableToCompose -> None
-      ) todo_list
+                  (src,tgt,c_uri,named_obj))::acc
+          with UnableToCompose -> acc
+      ) [] todo_list
     in
     new_coercions
   with ManglingFailed s -> HLog.error s; []
index 3a4dac726783e0e6584a8a772efc8d7f1c7aaaa4..9a1fdb0ea85de8434cf529ccfa183151960fb455 100644 (file)
 
 (* $Id$ *)
 
-type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+type coerc_carr = 
+  | Uri of UriManager.uri 
+  | Sort of Cic.sort 
+  | Term of Cic.term
+  | Fun of int 
+;;
+
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
 
@@ -56,6 +62,8 @@ let rec name_of_carr = function
   | Term t -> 
       prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); 
       "FixTheNameMangler"
+  | Fun i -> "FunClass_" ^ string_of_int i   
+;;
 
 let eq_carr src tgt =
   match src, tgt with
@@ -71,35 +79,54 @@ let eq_carr src tgt =
           (lazy ("Unsupported carr for coercions: " ^ 
           CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
       else raise EqCarrOnNonMetaClosed
+  | Fun _,Fun _ -> true (* only one Funclass? *)
+(*   | Fun i,Fun j when i=j -> true *)
   | _, _ -> false
+;;
 
 let to_list () =
-  !db
+  List.map (fun (s,t,l) -> s,t,List.map fst l) !db
+;;
 
 let rec myfilter p = function
   | [] -> []
   | (s,t,l)::tl ->
-      let l = List.filter (fun u -> not (p (s,t,u))) l in
+      let l = 
+        HExtlib.filter_map 
+          (fun (u,n) -> 
+            if p (s,t,u) then
+              if n = 1 then
+                None
+              else
+                Some (u,n-1)
+            else
+              Some (u,n)) 
+          l 
+      in
       if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
 ;;
   
 let remove_coercion p = db := myfilter p !db;;
 
 let find_coercion f =
-  List.flatten 
-    (List.map 
-      (fun (_,_,x) -> x) 
-      (List.filter (fun (s,t,_) -> f (s,t)) !db))
+    List.map
+    fst
+    (List.flatten
+    (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
 ;;
 
 let is_a_coercion u = 
-  List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db
+  List.exists 
+    (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl) 
+    !db
 ;;
 
 let get_carr uri =
   try
     let src, tgt, _ = 
-      List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !db 
+      List.find 
+        (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq uri x) xl) 
+        !db 
     in
     src, tgt
   with Not_found -> assert false (* uri must be a coercion *)
@@ -108,6 +135,7 @@ let get_carr uri =
 let term_of_carr = function
   | Uri u -> CicUtil.term_of_uri u
   | Sort s -> Cic.Sort s
+  | Fun _ -> assert false
   | Term _ -> assert false
 ;;
   
@@ -116,10 +144,18 @@ let add_coercion (src,tgt,u) =
   let where = List.filter (fun (s,t,_) -> f s t) !db in
   let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
   match where with
-  | [] -> db := (src,tgt,[u]) :: !db
+  | [] -> db := (src,tgt,[u,1]) :: !db
   | (src,tgt,l)::tl ->
       assert (tl = []); (* not sure, this may be a feature *)
-      db := (src,tgt,u::l)::tl @ rest
+      if List.exists (fun (x,_) -> UriManager.eq u x) l then
+        let l' = List.map 
+          (fun (x,n) -> if UriManager.eq u x then (x,n+1) else (x,n))
+          l
+        in
+        db := (src,tgt,l')::tl @ rest
+      else
+        db := (src,tgt,(u,1)::l)::tl @ rest
+      
 ;;
 
 
index 92d4b7f2484e231e1547a62899fe094ece785c79..d8a8b0574de506f222da61acfb073f9074723896 100644 (file)
@@ -36,6 +36,8 @@ type coerc_carr =
   | Uri of UriManager.uri (* const, mutind, mutconstr *)
   | Sort of Cic.sort (* Prop, Set, Type *) 
   | Term of Cic.term (* nothing supported *)
+  | Fun of int
+;;
   
 exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
index 40d6281252c58de143736f3e6aaaa9248c13d570..99ba33c33502c5f56f549d1bff2d716a103f7f4c 100644 (file)
@@ -37,7 +37,7 @@ let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion src tgt =
+let look_for_coercion' src tgt =
   let arity_of con =
     try
       let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
@@ -77,8 +77,16 @@ let look_for_coercion src tgt =
          None -> NoCoercion
        | Some ul ->
           let cl = List.map CicUtil.term_of_uri ul in
+          let funclass_arityl = 
+            let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+            List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+          in
           let arityl = List.map arity_of cl in
-          let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+          let argsl = 
+            List.map2 
+              (fun arity fn_arity -> 
+                mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl
+          in
           let newtl =
             List.map2 
               (fun args c -> 
@@ -96,7 +104,7 @@ let look_for_coercion src tgt =
 let look_for_coercion src tgt = 
   let src_uri = CoercDb.coerc_carr_of_term src in
   let tgt_uri = CoercDb.coerc_carr_of_term tgt in
-  look_for_coercion src_uri tgt_uri
+  look_for_coercion' src_uri tgt_uri
 
 let is_a_coercion t = 
   try
@@ -109,13 +117,15 @@ let source_of t =
     let uri = CicUtil.uri_of_term t in
     CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
   with Invalid_argument _ -> assert false (* t must be a coercion *)
-  
-let target_of t =
+
+let is_a_coercion_to_funclass t =
   try
     let uri = CicUtil.uri_of_term t in
-    CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
-  with Invalid_argument _ -> assert false (* t must be a coercion *)
-    
+    match snd (CoercDb.get_carr uri) with
+    | CoercDb.Fun i -> Some i
+    | _ -> None
+  with Invalid_argument _ -> None
+  
 let generate_dot_file () =
   let module Pp = GraphvizPp.Dot in
   let buf = Buffer.create 10240 in
@@ -145,5 +155,20 @@ let generate_dot_file () =
     l;
   Pp.trailer fmt;
   Buffer.contents buf
+;;
+    
+let is_composite t =
+  try
+    let uri = 
+      match t with 
+      | Cic.Appl (he::_) -> CicUtil.uri_of_term he
+      | _ -> CicUtil.uri_of_term t
+    in
+    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+    | Cic.Constant (_,_, _, _, attrs),_  ->
+        List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
+    | _ -> false
+  with Invalid_argument _ -> false
+;;
 
 (* EOF *)
index 01f3fecf69ab1d564f5910c6d60241e398d41fba..9e99d68f8cf02321645a9c4e3e88f3835070d779 100644 (file)
@@ -36,9 +36,18 @@ type coercion_search_result =
 val look_for_coercion :
   Cic.term -> Cic.term -> coercion_search_result
 
+val look_for_coercion' :
+  CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result
+
 val is_a_coercion: Cic.term -> bool
+val is_a_coercion_to_funclass: Cic.term -> int option
+
+(* checks if term is a constant or 
+ * a constant applyed that is marked with (`Class `Coercion) *)
+val is_composite: Cic.term -> bool
+
+
 val source_of: Cic.term -> Cic.term
-val target_of: Cic.term -> Cic.term
 
 val generate_dot_file: unit -> string
 
index 1db8f0cfc2c7b8374b79ae334ef068da0cab6c83..9529375ae57a6b36c3317c45b8878ff24fa6932e 100644 (file)
@@ -209,7 +209,7 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri =
+let add_coercion ~add_composites refinement_toolkit uri arity =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -225,23 +225,44 @@ let add_coercion ~add_composites refinement_toolkit uri =
    * should we saturate it with metas in case we insert it?
    * 
    *)
-  let extract_last_two_p ty =
+  let spline2list ty =
     let rec aux = function
-      | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> 
-          aux t
-      | Cic.Prod( _, src, tgt) -> src, tgt
-      | _ -> assert false
+      | Cic.Prod( _, src, tgt) -> src::aux tgt
+      | t -> [t]
     in
     aux ty
   in
+  let src_carr, tgt_carr = 
+    let list_remove_from_tail n l = 
+      let rec aux n = function
+        | hd::tl when n > 0 -> aux (n-1) tl
+        | l when n = 0 -> l
+        | _ -> assert false
+      in
+      aux n (List.rev l)
+    in
+    let types = spline2list coer_ty in
+    match arity, list_remove_from_tail arity types with
+    | 0,tgt::src::_ -> 
+        (* if ~delta is true, it is impossible to define an identity coercion *)
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+    | n,_::src::_ -> 
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+        CoercDb.Fun arity
+    | _ -> assert false    
+  in
   let already_in = 
      List.exists 
-      (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+      (fun (s,t,ul) -> 
+        List.exists 
+         (fun u -> 
+           UriManager.eq u uri && 
+           CoercDb.eq_carr s src_carr && 
+           CoercDb.eq_carr t tgt_carr) 
+         ul)
       (CoercDb.to_list ())
   in
-  let ty_src, ty_tgt = extract_last_two_p coer_ty in
-  let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
-  let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
   if not add_composites then
     (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
@@ -317,10 +338,13 @@ let remove_coercion uri =
 
 let generate_projections refinement_toolkit uri fields =
  let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
+ let projections = 
+   CicRecord.projections_of uri 
+     (List.map (fun (x,_,_) -> x) fields) 
+ in
   try
    List.iter2 
-    (fun (uri, name, bo) (_name, coercion) ->
+    (fun (uri, name, bo) (_name, coercion, arity) ->
       try
        let ty, ugraph =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
@@ -331,7 +355,8 @@ let generate_projections refinement_toolkit uri fields =
          if coercion then
             begin
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
-              let x = add_coercion ~add_composites:true refinement_toolkit uri
+              let x = 
+                add_coercion ~add_composites:true refinement_toolkit uri arity
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
index 61e2b2515ae9ba36837b142427cfd508b12014a5..06b1010ab500e05cd43aa0bbe1a8c08e6724de3e 100644 (file)
@@ -47,7 +47,7 @@ val remove_obj: UriManager.uri -> unit
 (* The list of added objects is returned.                                *)
 val add_coercion: 
   add_composites:bool -> 
-  RefinementTool.kit -> UriManager.uri -> 
+  RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
     UriManager.uri list
 
 (* inverse of add_coercion, removes both the eventually created composite   *)
index 6cab493fce46d067aa46c33f93d58d27e0a5d7f7..cb84601475f239463d668281bca7547583a1ef4a 100644 (file)
@@ -174,17 +174,21 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
 let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
   (metadata: MetadataTypes.constr list)
 =
-  let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables 
-  in
+  let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
   if (metadata = []) && concl_card = None && full_card = None then
-    failwith "MetadataQuery.at_least: no constraints given";
-  let (n,from,where) =
-    List.fold_left (add_constraint ~tables) (0,[],[]) metadata
-  in
-  let (n,from,where) =
-    add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
-  in
-  exec ~dbd ?rating (n,from,where)
+    begin
+      HLog.warn "MetadataConstraints.at_least: no constraints given";
+      []
+    end
+  else
+    let (n,from,where) =
+      List.fold_left (add_constraint ~tables) (0,[],[]) metadata
+    in
+    let (n,from,where) =
+      add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
+    in
+    exec ~dbd ?rating (n,from,where)
+;;
     
 let at_least  
   ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
index 91fa8004ca14ae49694c98209a751ffb765d2f2b..b393dbb91a8f0f0a3ca74983758e386c02738c3a 100644 (file)
@@ -132,7 +132,7 @@ struct
         (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
         assert false
     in
-    Pp.header ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
+    Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
     let rec aux =
       function
         | [] -> ()
index 9baf829ea940d2bad3c61d71ebfdea8781043f34..192460633d7577ff26a18e40d2d8ac4e8f699651 100644 (file)
@@ -419,8 +419,17 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
  =
   let module C = Cic in
    let curi,metasenv,pbo,pty = proof in
+   (* occur check *)
+   let occur i t =
+     let m = CicUtil.metas_of_term t in 
+     List.exists (fun (j,_) -> i=j) m
+   in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let _,_ = (* TASSI: FIXME *)
+   if occur metano term then
+     raise 
+       (ProofEngineTypes.Fail (lazy
+         "You can't letin a term containing the current goal"));
+    let _,_ =
       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
      let newmeta = new_meta_of_proof ~proof in
      let fresh_name =
index 4517db0b5eff1bfdfb7d11553ecc1c2910073fc7..862f781618cb55f34fed68f433970db769355490 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Aug 29 11:37:38 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Aug 31 14:46:00 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
index 12d302d244ab182a97981240dc66fe4141517257..27e7d4b9a28ed2caafb8477f7b54d898e0615884 100644 (file)
@@ -31,13 +31,12 @@ type attribute = string * string  (* <key, value> pair *)
 
 let png_flags = "-Tpng"
 let map_flags = "-Tcmapx"
-let tred_cmd = "tred" (* graphviz transitive reduction filter *)
 
 let tempfile () = Filename.temp_file "matita_" ""
 
 class type graphviz_widget =
   object
-    method load_graph_from_file: string -> unit
+    method load_graph_from_file: ?gviz_cmd:string -> string -> unit
     method connect_href:
       (GdkEvent.Button.t -> (string * string) list -> unit) -> unit
     method center_on_href: string -> unit
@@ -45,10 +44,10 @@ class type graphviz_widget =
     method as_viewport: GBin.viewport
   end
 
-class graphviz_impl ?packing gviz_cmd =
+class graphviz_impl ?packing () =
   let viewport = GBin.viewport ?packing () in
-  let mk_gviz_cmd flags src_fname dest_fname =
-    sprintf "cat %s | %s | %s %s > %s" src_fname tred_cmd gviz_cmd flags
+  let mk_gviz_cmd gviz_cmd flags src_fname dest_fname =
+    sprintf "cat %s | %s %s > %s" src_fname gviz_cmd flags
       dest_fname in
   let image =
     GMisc.image ~packing:viewport#add ~xalign:0. ~yalign:0. ~xpad:0 ~ypad:0 ()
@@ -70,9 +69,9 @@ class graphviz_impl ?packing gviz_cmd =
         (try href_cb button (self#find_href x y) with Not_found -> ());
         false))
 
-    method load_graph_from_file fname =
+    method load_graph_from_file ?(gviz_cmd = "dot") fname =
       let tmp_png = tempfile () in
-      let rc = Sys.command (mk_gviz_cmd png_flags fname tmp_png) in
+      let rc = Sys.command (mk_gviz_cmd gviz_cmd png_flags fname tmp_png) in
       if rc <> 0 then
         eprintf
           ("Graphviz command failed (exit code: %d) on the following graph:\n"
@@ -81,7 +80,7 @@ class graphviz_impl ?packing gviz_cmd =
       image#set_file tmp_png;
       HExtlib.safe_remove tmp_png;
       let tmp_map = tempfile () in
-      ignore (Sys.command (mk_gviz_cmd map_flags fname tmp_map));
+      ignore (Sys.command (mk_gviz_cmd gviz_cmd map_flags fname tmp_map));
       self#load_map tmp_map;
       HExtlib.safe_remove tmp_map
 
@@ -128,12 +127,6 @@ class graphviz_impl ?packing gviz_cmd =
 
   end
 
-let factory cmd ?packing () =
-  (new graphviz_impl ?packing cmd :> graphviz_widget)
-
-let gDot = factory "dot"
-let gNeato = factory "neato"
-let gTwopi = factory "twopi"
-let gCirco = factory "circo"
-let gFdp = factory "fdp"
+let graphviz ?packing () =
+  (new graphviz_impl ?packing () :> graphviz_widget)
 
index d6b7f4f6ee1a48043dd1151443266052d372e94b..7b90eec12e9c60c486fcb21a286e3e7c3f00d7a5 100644 (file)
@@ -38,8 +38,13 @@ class type graphviz_widget =
       *    GtkImage widget
       * 2) render it to a (HTML) map, internalizing its data.
       * Remember that map entries are generated only for nodes, (edges, ...)
-      * that have an "href" (or "URL", a synonym) attribute *)
-    method load_graph_from_file: string -> unit
+      * that have an "href" (or "URL", a synonym) attribute 
+      * Interesting values for gviz_cmd are:
+      *   'neato'
+      *   'dot'
+      *   'tred | dot'
+      *)
+    method load_graph_from_file: ?gviz_cmd:string -> string -> unit
 
     (** Callback invoked when a click on a node listed in the map is received.
      * @param gdk's button event
@@ -63,9 +68,5 @@ class type graphviz_widget =
 
 (** {2 Constructors} *)
 
-val gDot: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gNeato: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gTwopi: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gCirco: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gFdp: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
+val graphviz: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
 
index 31a5f35ee289ee6e4bf9ec199b869c327dc388a7..9860c63e29137b8c4d1d409d6ac18486ea03574a 100644 (file)
@@ -19,9 +19,9 @@ default "equality"
  cic:/Coq/Init/Logic/sym_eq.con
  cic:/Coq/Init/Logic/trans_eq.con
  cic:/Coq/Init/Logic/eq_ind.con
- cic:/Coq/Init/Logic/eq_ind_r.con 
- cic:/Coq/Init/Logic/f_equal.con 
- cic:/Coq/Init/Logic/f_equal1.con. 
+ cic:/Coq/Init/Logic/eq_ind_r.con
+ cic:/Coq/Init/Logic/f_equal.con
+ cic:/matita/legacy/coq/f_equal1.con.
 
 default "true"
  cic:/Coq/Init/Logic/True.ind. 
@@ -75,17 +75,16 @@ interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/n
 interpretation "Coq's natural 'not less or equal than'"
  'nleq x y = (cic:/Coq/Init/Logic/not.con 
                (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)).
-
+               
+theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A.
+  x = y \to (f y) = (f x).
+  intros.
+  symmetry.
+  apply cic:/Coq/Init/Logic/f_equal.con.
+  assumption.
+qed.
 (* aliases *)
 
 (* FG: This is because "and" is a reserved keyword of the parser *)
 alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
 
-(* theorems *)
-
-theorem f_equal1 : 
-  \forall A,B:Type. \forall f:A \to B. \forall x,y:A.
-  x = y \to f y = f x.
-  intros.elim H.reflexivity.
-qed.
-
index 129b00189f1e61523c1b446bcd1c01ce0981d531..c26449c4261595031deaf05fd8b104816a384c18 100644 (file)
@@ -60,6 +60,14 @@ theorem eq_elim_r:
 intros. elim (sym_eq ? ? ? H1).assumption.
 qed.
 
+theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
+\forall x,y:A. x=y \to f x = f y.
+intros.elim H.reflexivity.
+qed.
+
+coercion cic:/matita/logic/equality/sym_eq.con.
+coercion cic:/matita/logic/equality/eq_f.con.
+
 default "equality"
  cic:/matita/logic/equality/eq.ind
  cic:/matita/logic/equality/sym_eq.con
@@ -67,19 +75,8 @@ default "equality"
  cic:/matita/logic/equality/eq_ind.con
  cic:/matita/logic/equality/eq_elim_r.con
  cic:/matita/logic/equality/eq_f.con
- cic:/matita/logic/equality/eq_f1.con. (* \x.sym (eq_f x) *)
-
+ cic:/matita/logic/equality/eq_OF_eq.con. (* \x.sym (eq_f x) *)
  
-theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
-\forall x,y:A. x=y \to f x = f y.
-intros.elim H.reflexivity.
-qed.
-
-theorem eq_f1: \forall  A,B:Type.\forall f:A\to B.
-\forall x,y:A. x=y \to f y = f x.
-intros.elim H.reflexivity.
-qed.
-
 theorem eq_f2: \forall  A,B,C:Type.\forall f:A\to B \to C.
 \forall x1,x2:A. \forall y1,y2:B.
 x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
index c235a9f4354402669ac495ea0f500f2064945504..6976d57e05462fdfca54bd3ff8a1d3470c5fcd23 100644 (file)
@@ -797,7 +797,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
   let gui = get_gui () in
   let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
-  let gviz = LablGraphviz.gDot ~packing:win#graphScrolledWin#add () in
+  let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
   let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
   let combo,_ = GEdit.combo_box_text ~strings:queries () in
   let activate_combo_query input q =
@@ -1053,7 +1053,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let fmt = Format.formatter_of_out_channel oc in
       MetadataDeps.DepGraph.render fmt gviz_graph;
       close_out oc;
-      gviz#load_graph_from_file tmpfile;
+      gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
       (match center_on with
       | None -> ()
       | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
index 914126de2454d4804dfc6909837254f6d6417c68..e792bd78010b3a67a87f3455be0ff3998f5e891b 100644 (file)
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/coercions/".
-include "nat/nat.ma".
+
+include "nat/compare.ma".
+include "datatypes/bool.ma".
 
 inductive pos: Set \def
 | one : pos
 | next : pos \to pos.
 
-inductive nat:Set \def
-| O : nat
-| S : nat \to nat.
-
 inductive int: Set \def
 | positive: nat \to int
 | negative : nat \to int.
@@ -60,11 +58,6 @@ definition double2:
   \forall f:int \to int. pos \to int 
 \def 
   \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)).
-  
-coercion cic:/matita/logic/equality/eq_f.con.  
-coercion cic:/matita/logic/equality/eq_f1.con.
-variant xxx : ? \def eq_f.
-coercion cic:/matita/tests/coercions/xxx.con.
 
 theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
   intros.
@@ -73,8 +66,6 @@ qed.
 
 variant pos2nat' : ? \def pos2nat.
 
-coercion cic:/matita/tests/coercions/xxx.con.
-
 inductive initial: Set \def iii : initial.
 
 definition i2pos: ? \def \lambda x:initial.one.
@@ -83,4 +74,39 @@ coercion cic:/matita/tests/coercions/i2pos.con.
 
 coercion cic:/matita/tests/coercions/pos2nat'.con.
 
+inductive listn (A:Type) : nat \to Type \def
+ | Nil : listn A O
+ | Next : \forall n.\forall l:listn A n.\forall a:A.listn A (S n).
+definition if : \forall A:Type.\forall b:bool.\forall a,c:A.A \def
+  \lambda A,b,a,c.
+  match b with
+  [ true \Rightarrow a
+  | false \Rightarrow c].  
+let rec ith (A:Type) (n,m:nat) (dummy:A) (l:listn A n) on l \def
+  match l with
+  [ Nil \Rightarrow dummy
+  | (Next w l x) \Rightarrow if A (eqb w m) x (ith A w m dummy l)].  
+
+definition listn2function: 
+  \forall A:Type.\forall dummy:A.\forall n.listn A n \to nat \to A
+\def
+  \lambda A,dummy,n,l,m.ith A n m dummy l.
+  
+definition natlist2map: ? \def listn2function nat O.
+  
+coercion cic:/matita/tests/coercions/natlist2map.con 1.
+definition map:  \forall n:nat.\forall l:listn nat n. nat \to nat \def
+  \lambda n:nat.\lambda l:listn nat n.\lambda m:nat.l m.
+  
+definition church: nat \to nat \to nat \def times.
+
+coercion cic:/matita/tests/coercions/church.con 1.
+
+definition mapmult:  \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def
+  \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.l m o.
 
+  
+  
\ No newline at end of file