X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=9fd6ec52a1ec62c9c24991bc1f91f1a4ebc337ea;hb=a9e833b37216b225262450fd4e3fa5bf79ae4c3a;hp=fc8bd12bae19c94b76a87c2328d7abb5e89cd868;hpb=5b6965fc326021ec30894846113665d1b01fe8ee;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index fc8bd12ba..9fd6ec52a 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -33,7 +33,16 @@
  exception ExplicitNamedSubstitutionAppliedToRel;;
  exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
  
- let uri_of_id_map = Hashtbl.create 53;;
+ (* merge removing duplicates of two lists free of duplicates *)
+ let union dom1 dom2 =
+  let rec filter =
+   function
+      [] -> []
+    | he::tl ->
+       if List.mem he dom1 then filter tl else he::(filter tl)
+  in
+   dom1 @ (filter dom2)
+ ;;
 
  let get_index_in_list e =
   let rec aux i =
@@ -75,6 +84,12 @@
     aux (1,canonical_context)
  ;;
 
+ let deoptionize_exp_named_subst =
+  function
+     None -> [], (function _ -> [])
+   | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
+ ;;
+
  let term_of_con_uri uri exp_named_subst =
   Const (uri,exp_named_subst)
  ;;
@@ -93,30 +108,29 @@
 
  let term_of_uri uri =
   match uri with
-     CicTextualParser0.ConUri uri -> term_of_con_uri uri
-   | CicTextualParser0.VarUri uri -> term_of_var_uri uri
-   | CicTextualParser0.IndTyUri (uri,tyno) -> term_of_indty_uri (uri,tyno) 
+     CicTextualParser0.ConUri uri ->
+      term_of_con_uri uri
+   | CicTextualParser0.VarUri uri ->
+      term_of_var_uri uri
+   | CicTextualParser0.IndTyUri (uri,tyno) ->
+      term_of_indty_uri (uri,tyno) 
    | CicTextualParser0.IndConUri (uri,tyno,consno) ->
       term_of_indcon_uri (uri,tyno,consno)
  ;;
 
- let var_uri_of_id id =
-  try
-   (match Hashtbl.find uri_of_id_map id with
-       CicTextualParser0.VarUri uri -> uri
-     | _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
-   )
-  with
-   Not_found ->
-    match !CicTextualParser0.locate_object id with
-       None -> raise (UnknownIdentifier id)
-     | Some (CicTextualParser0.VarUri uri as varuri) ->
-        Hashtbl.add uri_of_id_map id varuri;
-        uri
-     | Some _ ->
-        raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+ let var_uri_of_id id interp =
+  match interp id with
+     None -> raise (UnknownIdentifier id)
+   | Some (CicTextualParser0.VarUri uri) -> uri
+   | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
  ;;
 
+ let indty_uri_of_id id interp =
+  match interp id with
+     None -> raise (UnknownIdentifier id)
+   | Some (CicTextualParser0.IndTyUri (uri,tyno)) -> (uri,tyno)
+   | Some _ -> raise InductiveTypeURIExpected
+ ;;
 %}
 %token <string> ID
 %token <int> META
@@ -130,94 +144,120 @@
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
-%type <Cic.term option> main
+%type <string list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
 %%
 main:
-   expr  { Some $1 }
- | alias { None }
- | EOF   { raise CicTextualParser0.Eof }
+ expr EOF { $1 }
 ;
 expr2:
    CONURI exp_named_subst
-   { term_of_con_uri $1 $2 }
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
+   }
  | VARURI exp_named_subst
-   { term_of_var_uri $1 $2 }
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
+   }
  | INDTYURI exp_named_subst
-   { term_of_indty_uri $1 $2 }
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
+   }
  | INDCONURI exp_named_subst
-   { term_of_indcon_uri $1 $2 }
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
+   }
  | ID exp_named_subst
    { try
       let res =
        Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
       in
-       if $2 = [] then res else raise (ExplicitNamedSubstitutionAppliedToRel)
+       (match $2 with
+           None -> ([], function _ -> res)
+         | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
+       )
      with
       Not_found ->
-       try
-        term_of_uri (Hashtbl.find uri_of_id_map $1) $2
-       with
-        Not_found ->
-	 match !CicTextualParser0.locate_object $1 with
-	  | None      -> raise (UnknownIdentifier $1)
-	  | Some uri ->
-             Hashtbl.add uri_of_id_map $1 uri;
-             term_of_uri uri $2
+       let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+        let dom = union dom1 [$1] in
+         dom,
+          function interp ->
+           match interp $1 with
+	      None  -> raise (UnknownIdentifier $1)
+	    | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
-    { MutCase (fst $5, snd $5, $7, $3, $10) }
+    { let dom1,mk_expr1 = $3 in
+      let dom2,mk_expr2 = $7 in
+      let dom3,mk_expr3 = $10 in
+       let dom = union dom1 (union dom2 dom3) in
+        dom,
+        function interp ->
+         MutCase
+          (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
+    }
  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
-    { try
-       let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
-        raise InductiveTypeURIExpected
-      with
-       Not_found ->
-        match Hashtbl.find uri_of_id_map $5 with
-           CicTextualParser0.IndTyUri (uri,typeno) ->
-            MutCase (uri, typeno, $7, $3, $10)
-         | _ -> raise InductiveTypeURIExpected
+    { let dom1,mk_expr1 = $3 in
+      let dom2,mk_expr2 = $7 in
+      let dom3,mk_expr3 = $10 in
+       let dom = union [$5] (union dom1 (union dom2 dom3)) in
+        dom,
+        function interp ->
+         let uri,typeno = indty_uri_of_id $5 interp in
+          MutCase
+           (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
+             (mk_expr3 interp))
     }
  | fixheader LCURLY exprseplist RCURLY
-    { let fixfunsdecls = snd $1 in
-      let fixfunsbodies = $3 in
-       let idx =
-        let rec find idx =
-         function
-            [] -> raise Not_found
-          | (name,_,_)::_  when name = (fst $1) -> idx
-          | _::tl -> find (idx+1) tl
-        in
-         find 0 fixfunsdecls
-       in
-        let fixfuns =
-         List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
-          fixfunsdecls fixfunsbodies
-        in
-         for i = 1 to List.length fixfuns do
-          CicTextualParser0.binders := List.tl !CicTextualParser0.binders
-         done ;
-         Fix (idx,fixfuns)
+    { let dom1,mk_fixheader = $1 in
+      let dom2,mk_exprseplist = $3 in
+       let dom = union dom1 dom2 in
+        dom,
+         function interp ->
+          let fixfunsdecls = snd (mk_fixheader interp) in
+          let fixfunsbodies = (mk_exprseplist interp) in
+           let idx =
+            let rec find idx =
+             function
+                [] -> raise Not_found
+              | (name,_,_)::_  when name = (fst (mk_fixheader interp)) -> idx
+              | _::tl -> find (idx+1) tl
+            in
+             find 0 fixfunsdecls
+           in
+            let fixfuns =
+             List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
+              fixfunsdecls fixfunsbodies
+            in
+             for i = 1 to List.length fixfuns do
+              CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+             done ;
+             Fix (idx,fixfuns)
     }
  | cofixheader LCURLY exprseplist RCURLY
-    { let cofixfunsdecls = (snd $1) in
-      let cofixfunsbodies = $3 in
-       let idx =
-        let rec find idx =
-         function
-            [] -> raise Not_found
-          | (name,_)::_  when name = (fst $1) -> idx
-          | _::tl -> find (idx+1) tl
-        in
-         find 0 cofixfunsdecls
-       in
-        let cofixfuns =
-         List.map2 (fun (name,ty) bo -> (name,ty,bo))
-          cofixfunsdecls cofixfunsbodies
-        in
-         for i = 1 to List.length cofixfuns do
-          CicTextualParser0.binders := List.tl !CicTextualParser0.binders
-         done ;
-         CoFix (idx,cofixfuns)
+    { let dom1,mk_cofixheader = $1 in
+      let dom2,mk_exprseplist = $3 in
+       let dom = union dom1 dom2 in
+        dom,
+         function interp ->
+          let cofixfunsdecls = (snd (mk_cofixheader interp)) in
+          let cofixfunsbodies = mk_exprseplist interp in
+           let idx =
+            let rec find idx =
+             function
+                [] -> raise Not_found
+              | (name,_)::_  when name = (fst (mk_cofixheader interp)) -> idx
+              | _::tl -> find (idx+1) tl
+            in
+             find 0 cofixfunsdecls
+           in
+            let cofixfuns =
+             List.map2 (fun (name,ty) bo -> (name,ty,bo))
+              cofixfunsdecls cofixfunsbodies
+            in
+             for i = 1 to List.length cofixfuns do
+              CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+             done ;
+             CoFix (idx,cofixfuns)
     }
  | IMPLICIT
     { let newmeta = new_meta () in
@@ -230,119 +270,210 @@ expr2:
            newmeta+1, new_canonical_context, Meta (newmeta,irl);
            newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
           ] @ !CicTextualParser0.metasenv ;
-         Meta (newmeta+2,irl)
+         [], function _ -> Meta (newmeta+2,irl)
+    }
+ | SET  { [], function _ -> Sort Set }
+ | PROP { [], function _ -> Sort Prop }
+ | TYPE { [], function _ -> Sort Type }
+ | LPAREN expr CAST expr RPAREN
+    { let dom1,mk_expr1 = $2 in
+      let dom2,mk_expr2 = $4 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
+    }
+ | META LBRACKET substitutionlist RBRACKET
+    { let dom,mk_substitutionlist = $3 in
+       dom, function interp -> Meta ($1, mk_substitutionlist interp)
+    } 
+ | LPAREN expr expr exprlist RPAREN
+    { let dom1,mk_expr1 = $2 in
+      let dom2,mk_expr2 = $3 in
+      let dom3,mk_exprlist = $4 in
+       let dom = union dom1 (union dom2 dom3) in
+        dom,
+         function interp ->
+          Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp))
     }
- | SET { Sort Set }
- | PROP { Sort Prop }
- | TYPE { Sort Type }
- | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } 
- | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
 ;
 exp_named_subst :
-    { [] }
+    { None }
  | LCURLY named_substs RCURLY
-    { $2 }
+    { Some $2 }
 ;
 named_substs :
    VARURI LETIN expr2
-    { [$1,$3] }
+    { let dom,mk_expr = $3 in
+       dom, function interp -> [$1, mk_expr interp] }
  | ID LETIN expr2
-    { [var_uri_of_id $1,$3] }
+    { let dom1,mk_expr = $3 in
+       let dom = union [$1] dom1 in
+        dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
  | VARURI LETIN expr2 SEMICOLON named_substs
-    { ($1,$3)::$5 }
+    { let dom1,mk_expr = $3 in
+      let dom2,mk_named_substs = $5 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
+    }
  | ID LETIN expr2 SEMICOLON named_substs
-    { (var_uri_of_id $1,$3)::$5 }
+    { let dom1,mk_expr = $3 in
+      let dom2,mk_named_substs = $5 in
+       let dom = union [$1] (union dom1 dom2) in
+        dom,
+         function interp ->
+          (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
+    }
 ;
 expr :
    pihead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      Prod (fst $1, snd $1,$2) }
+      let dom1,mk_expr1 = snd $1 in
+      let dom2,mk_expr2 = $2 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
+    }
  | lambdahead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      Lambda (fst $1, snd $1,$2) }
+      let dom1,mk_expr1 = snd $1 in
+      let dom2,mk_expr2 = $2 in
+       let dom = union dom1 dom2 in
+        dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
+    }
  | letinhead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      LetIn (fst $1, snd $1,$2) }
+      let dom1,mk_expr1 = snd $1 in
+      let dom2,mk_expr2 = $2 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
+    }
  | expr2
     { $1 }
 ;
 fixheader:
    FIX ID LCURLY fixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
-       CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-       $2,$4
+    { let dom,mk_fixfunsdecl = $4 in
+       dom,
+        function interp ->
+         let bs =
+          List.rev_map
+           (function (name,_,_) -> Some (Name name)) (mk_fixfunsdecl interp)
+         in
+          CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+          $2,(mk_fixfunsdecl interp)
     }
 ;
 fixfunsdecl:
    ID LPAREN NUM RPAREN COLON expr
-    { [$1,$3,$6] }
+    { let dom,mk_expr = $6 in
+       dom, function interp -> [$1,$3,mk_expr interp]
+    }
  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
-    { ($1,$3,$6)::$8 }
+    { let dom1,mk_expr = $6 in
+      let dom2,mk_fixfunsdecl = $8 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
+    }
 ;
 cofixheader:
    COFIX ID LCURLY cofixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
-       CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-       $2,$4
+    { let dom,mk_cofixfunsdecl = $4 in
+       dom,
+        function interp ->
+         let bs =
+          List.rev_map
+           (function (name,_) -> Some (Name name)) (mk_cofixfunsdecl interp)
+         in
+          CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+          $2,(mk_cofixfunsdecl interp)
     }
 ;
 cofixfunsdecl:
    ID COLON expr
-    { [$1,$3] }
+    { let dom,mk_expr = $3 in
+       dom, function interp -> [$1,(mk_expr interp)]
+    }
  | ID COLON expr SEMICOLON cofixfunsdecl
-    { ($1,$3)::$5 }
+    { let dom1,mk_expr = $3 in
+      let dom2,mk_cofixfunsdecl = $5 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
+    }
 ;
 pihead:
    PROD ID COLON expr DOT
     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
-      (Cic.Name $2, $4) }
+      let dom,mk_expr = $4 in
+       Cic.Name $2, (dom, function interp -> mk_expr interp)
+    }
  | expr2 ARROW
    { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
-     (Anonymous, $1) }
+     let dom,mk_expr = $1 in
+      Anonymous, (dom, function interp -> mk_expr interp)
+   }
  | LPAREN expr RPAREN ARROW
    { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
-     (Anonymous, $2) }
+     let dom,mk_expr = $2 in
+      Anonymous, (dom, function interp -> mk_expr interp)
+   }
 ;
 lambdahead:
   LAMBDA ID COLON expr DOT
    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
-     (Cic.Name $2, $4) }
+     let dom,mk_expr = $4 in
+      Cic.Name $2, (dom, function interp -> mk_expr interp)
+   }
 ;
 letinhead:
   LAMBDA ID LETIN expr DOT
    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
-     (Cic.Name $2, $4) }
+     let dom,mk_expr = $4 in
+      Cic.Name $2, (dom, function interp -> mk_expr interp)
+   }
 ;
 branches:
-                            { [] }
- | expr SEMICOLON branches  { $1::$3 }
- | expr                     { [$1] }
+    { [], function _ -> [] }
+ | expr SEMICOLON branches
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_branches = $3 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> (mk_expr interp)::(mk_branches interp)
+    }
+ | expr
+    { let dom,mk_expr = $1 in
+       dom, function interp -> [mk_expr interp]
+    }
 ;
 exprlist:
-                  { [] }
- | expr exprlist  { $1::$2 }
+    
+    { [], function _ -> [] }
+ | expr exprlist
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_exprlist = $2 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
+    }
 ;
 exprseplist:
-   expr                        { [$1] }
- | expr SEMICOLON exprseplist  { $1::$3 }
+   expr
+    { let dom,mk_expr = $1 in
+       dom, function interp -> [mk_expr interp]
+    }
+ | expr SEMICOLON exprseplist
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_exprseplist = $3 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
+    }
 ;
 substitutionlist:
-                                     { [] }
- | expr SEMICOLON substitutionlist   { (Some $1)::$3 }
- | NONE SEMICOLON substitutionlist   { None::$3 }
-;
-alias:
-   ALIAS ID CONURI
-    { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.ConUri $3) }
- | ALIAS ID VARURI
-    { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.VarUri $3) }
- | ALIAS ID INDTYURI
-    { Hashtbl.add uri_of_id_map $2
-       (CicTextualParser0.IndTyUri (fst $3, snd $3))
+    { [], function _ -> [] }
+ | expr SEMICOLON substitutionlist
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_substitutionlist = $3 in
+       let dom = union dom1 dom2 in
+        dom,
+         function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
     }
- | ALIAS ID INDCONURI
-    { let uri,indno,consno = $3 in
-       Hashtbl.add uri_of_id_map $2
-        (CicTextualParser0.IndConUri (uri, indno, consno))
+ | NONE SEMICOLON substitutionlist
+    { let dom,mk_exprsubstitutionlist = $3 in
+       dom, function interp -> None::(mk_exprsubstitutionlist interp)
     }